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

Proc index in the formula

Browse Source
This commit is contained in:
Artur Meski
2023-09-15 14:54:04 +01:00
parent 282f50bbf8
commit 1488ad1501
1 changed files with 2 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
examples/bdd/generators/gen_drs.py
View File

@@ -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]( "