artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

asm, epistemic properties

Browse Source
This commit is contained in:
Artur Meski
2018-12-02 20:49:18 +00:00
parent 215015df57
commit 9ac04da320
1 changed files with 7 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
in/scripts/gen_asm.py
View File

@@ -64,13 +64,13 @@ init_trans = 8*" " + "{ proc1={a} }: init -> act;\n"
transitions += init_trans
for i in range(1, n+1):
transitions += "{:s}{{ proc{:d}={{}} }}: act -> act;\n".format(8*" ", i, i)
transitions += "{:s}{{ proc{:d}={{}} }}: act -> act : ~proc{:d}.dy;\n".format(8*" ", i, i, i)
for i in range(2, n+1):
transitions += "{:s}{{ proc{:d}={{a}} }}: act -> act : proc{:d}.dy;\n".format(8*" ", i, i-1)
final_cond = "proc1.dy"
for i in range(1, n+1):
for i in range(2, n+1):
final_cond += " AND proc{:d}.dy".format(i)
transitions += "{:s}{{ procFinal={{done}} }}: act -> act : {:s};\n".format(8*" ", final_cond)
@@ -82,8 +82,12 @@ formula = "EF( procFinal.done )"
out += PROPERTY_STR.format("f1",formula)
# f2
formula = "EF( ~procFinal.done )"
formula = "AG( proc{:d}.d IMPLIES K[proc{:d}]( proc{:d}.y ) )".format(n, n, n-1)
out += PROPERTY_STR.format("f2",formula)
# x1
formula = "EF( ~procFinal.done )"
out += PROPERTY_STR.format("x1",formula)
print(out)