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

script

Browse Source
This commit is contained in:
Artur Meski
2018-11-05 13:25:57 +00:00
parent 66f9e36c5d
commit ff0031244e
1 changed files with 12 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
in/scripts/gen_tgc_sc.py
View File

@@ -81,16 +81,12 @@ out += CA_STR.format(transitions)
# f1 # f1
formula = "EF( proc0.in )" formula = "EF( proc0.in )"
for i in range(1, n):
formula += " AND EF( proc{:d}.in )".format(i)
out += PROPERTY_STR.format("f1",formula) out += PROPERTY_STR.format("f1",formula)
# f2 # f2
subf = "~proc1.in" formula = "EF( proc0.in )"
for i in range(2, n): for i in range(1, n):
subf += " AND ~proc{:d}.in".format(i) formula += " AND EF( proc{:d}.in )".format(i)
formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
out += PROPERTY_STR.format("f2",formula) out += PROPERTY_STR.format("f2",formula)
# f3 # f3
@@ -100,4 +96,13 @@ for i in range(1, n):
formula += " )" formula += " )"
out += PROPERTY_STR.format("f3",formula) out += PROPERTY_STR.format("f3",formula)
# f4
subf = "~proc1.in"
for i in range(2, n):
subf += " AND ~proc{:d}.in".format(i)
formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
out += PROPERTY_STR.format("f4",formula)
print(out) print(out)