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

SmtCheckerPGRS -> ..RS; new: SmtCheckerRSNA

Browse Source
This commit is contained in:
Artur Meski
2016-12-28 22:13:16 +01:00
parent 5ddc549245
commit 5e8417baf2
6 changed files with 292 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
rs_testing.py
View File

@@ -32,9 +32,12 @@ def test_extended_automaton():
na = NetworkOfContextAutomata([c1,c2])
rc = ReactionSystemWithAutomaton(r,na)
rna = ReactionSystemWithAutomaton(r,na)
rc.show()
rna.show()
checker = SmtCheckerRS(rna)
def process():
@@ -44,15 +47,15 @@ def process():
# PGRS:
# RS:
# rsca = rs_examples.ca_toy_ex1()
# rsca.show()
# smt = SmtCheckerPGRS(rsca)
# smt = SmtCheckerRS(rsca)
# smt.check_reachability(rs_examples.ca_toy_ex1_property1(), print_time=True)
# rsca = rs_examples.ca_bitctr(N)
# rsca.show(True)
# smt = SmtCheckerPGRS(rsca)
# smt = SmtCheckerRS(rsca)
# smt.check_reachability(rs_examples.ca_bitctr_property(N), print_time=True)
# Distributed RS: