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

encoder

Browse Source
This commit is contained in:
Artur Meski
2017-03-03 20:08:06 +01:00
parent ed1d9433a6
commit 9fb4e4a343
1 changed files with 7 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
logics/rsltl.py
View File

@@ -125,5 +125,10 @@ class Formula_rsLTL(object):
#x = ~( FormulaLTL.f_X(BagDescription.f_TRUE(), FormulaLTL.f_bag( ~((BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) ) ) ) & FormulaLTL.f_X(BagDescription.f_TRUE(), FormulaLTL.f_bag( ~((BagDescription.f_entity("ent3") == 1) ) ) ) #x = ~( FormulaLTL.f_X(BagDescription.f_TRUE(), FormulaLTL.f_bag( ~((BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) ) ) ) & FormulaLTL.f_X(BagDescription.f_TRUE(), FormulaLTL.f_bag( ~((BagDescription.f_entity("ent3") == 1) ) ) )
#print(x) #print(x)
class Encoder_rsLTL(object):
"""Class for encoding rsLTL formulae for a given smt_checker instance"""
def __init__(self, smt_checker):
self.smt_checker = smt_checker