From 1488ad150115d9fd500540c0b5d2571a37c98664 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 15 Sep 2023 14:54:04 +0100 Subject: [PATCH] Proc index in the formula --- examples/bdd/generators/gen_drs.py | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/examples/bdd/generators/gen_drs.py b/examples/bdd/generators/gen_drs.py index 67450d7..99f8a03 100755 --- a/examples/bdd/generators/gen_drs.py +++ b/examples/bdd/generators/gen_drs.py @@ -257,10 +257,8 @@ class DRSGenerator: def generate_formula(self): - r = "rsctlk-property { f4 : AG( proc0.in IMPLIES C[proc0,proc1,proc2](~proc1.in AND ~proc2.in) ) };" - - disjunction = " OR ".join([f"proc{i}.TF" for i in range(1, self.x + 1)]) - conjunction = " AND ".join([f"~proc{i}.TF" for i in range(1, self.x + 1)]) + disjunction = " OR ".join([f"proc{i}.TF" for i in range(1, self.y + 1)]) + conjunction = " AND ".join([f"~proc{i}.TF" for i in range(1, self.y + 1)]) r = ( "rsctlk-property { f0 : AG( K[proc0]( "