From 1f132d4692b0538fd4d8a056db7af89849ba6254 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 25 Nov 2018 15:11:56 +0000 Subject: [PATCH] Formula --- in/scripts/gen_tgc_sc.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/in/scripts/gen_tgc_sc.py b/in/scripts/gen_tgc_sc.py index c60637b..d0b18d8 100755 --- a/in/scripts/gen_tgc_sc.py +++ b/in/scripts/gen_tgc_sc.py @@ -101,8 +101,17 @@ 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) +# f5 +subf = "~proc1.in" +for i in range(2, n): + subf += " AND ~proc{:d}.in".format(i) +all_agents = "proc0" +for i in range(1, n): + all_agents += ",proc{:d}".format(i) +formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents,subf) +out += PROPERTY_STR.format("f5",formula) + print(out)