bitctr

rctsys.py

@@ -230,10 +230,13 @@ class ReactionSystem(object):
         s = s[:-2]
         return s
 
-    def show_reactions(self):
+    def show_reactions(self, soft=False):
         print("[*] Reactions:")
-        for reaction in self.reactions:
+        if soft and len(self.reactions) > 50:
-            print("\t - ( R={" + self.entities_ids_set_to_str(reaction[0]) + "}, \tI={" + self.entities_ids_set_to_str(reaction[1]) + "}, \tP={" + self.entities_ids_set_to_str(reaction[2]) + "} )")
+            print("\t -> there are more than 50 reactions (" + str(len(self.reactions)) + ")")
+        else:
+            for reaction in self.reactions:
+                print("\t - ( R={" + self.entities_ids_set_to_str(reaction[0]) + "}, \tI={" + self.entities_ids_set_to_str(reaction[1]) + "}, \tP={" + self.entities_ids_set_to_str(reaction[2]) + "} )")
 
     def show_background_set(self):
         print("[*] Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")
@@ -248,11 +251,11 @@ class ReactionSystem(object):
         if len(self.context_entities) > 0:
             print("[*] Context entities: " + self.entities_ids_set_to_str(self.context_entities))
 
-    def show(self):
+    def show(self, soft=False):
 
         self.show_background_set()
         self.show_initial_contexts()
-        self.show_reactions()
+        self.show_reactions(soft)
         self.show_context_entities()
         
     def get_reactions_by_product(self):
@@ -304,8 +307,8 @@ class ReactionSystemWithAutomaton(object):
         self.rs = reaction_system
         self.ca = context_automaton
 
-    def show(self):
+    def show(self, soft=False):
-        self.rs.show()
+        self.rs.show(soft)
         self.ca.show()
         
     def sanity_check(self):

rs_examples.py

@@ -138,6 +138,68 @@ def ca_toy_ex1_property1():
     return ["e"]
 
 
+def ca_bitctr(bits):
+
+    rs = ReactionSystem()
+
+    n = bits
+
+    for i in range(0,bits):
+        rs.add_bg_set_entities(["p" + str(i)])
+
+    rs.add_bg_set_entities(["dec"])
+    rs.add_bg_set_entities(["inc"])
+
+    # (1) no dec, no inc
+    for j in range(0,bits):
+        rs.add_reaction(["p"+str(j)], ["dec","inc"], ["p"+str(j)])
+
+    # (2) increment
+    rs.add_reaction(["inc"],["dec","p0"],["p0"])
+    for j in range(1,bits):
+        R = ["inc"]
+        for k in range(0,j):
+            R.append("p"+str(k))
+        I = ["dec","p"+str(j)]
+        P = ["p"+str(j)]
+        rs.add_reaction(R, I, P)
+
+    for j in range(0,bits):
+        for k in range(j+1,bits):
+            rs.add_reaction(["inc","p"+str(k)], ["dec","p"+str(j)], ["p"+str(k)])
+
+    # (3) decrement
+    for j in range(0,bits):
+        R=["dec"]
+        I=["inc"]
+        for k in range(0,j+1):
+            I.append("p"+str(k))
+        P=["p"+str(j)]
+        rs.add_reaction(R, I, P)
+
+    for j in range(0,bits):
+        for k in range(j+1,bits):
+            rs.add_reaction(["dec","p"+str(j),"p"+str(k)], ["inc"], ["p"+str(k)])
+
+    ca = ContextAutomaton(rs)
+    ca.add_init_state("1")
+    ca.add_transition("1", ["inc"], "1")
+    ca.add_transition("1", ["inc","dec"], "1")
+    ca.add_transition("1", ["dec"], "1")
+    
+    rsca = ReactionSystemWithAutomaton(rs,ca)
+    
+    return rsca
+    
+def ca_bitctr_property(bits):
+    
+    state = []
+    
+    for i in range(0,bits):
+        state.append("p"+str(i))
+        
+    return state
+
 def drs_toy_ex1():
     
     drs = DistributedReactionSystem()

rssmt.py

@@ -36,30 +36,27 @@ def main():
         
     print(rsmc_banner)
 
-    #rs = rs_examples.toy_ex3()
-    #rs = rs_examples.bitctr(16)
-    
-    #smt = SmtChecker(rs)
-    #smt.check_reachability(["p0","p1","p2","p3","p4","p5","p6","p7","p8","p9","p10","p11","p12","p13","p14","p15"], print_time=True)
-    #smt.check_reachability(["1","3","4"], print_time=True)
-
     # PGRS:
     # rsca = rs_examples.ca_toy_ex1()
     # rsca.show()
     # smt = SmtCheckerPGRS(rsca)
     # smt.check_reachability(rs_examples.ca_toy_ex1_property1(), print_time=True)
 
-    # Distributed RS:
+    rsca = rs_examples.ca_bitctr(N)
+    rsca.show(True)
+    smt = SmtCheckerPGRS(rsca)
+    smt.check_reachability(rs_examples.ca_bitctr_property(N), print_time=True)
     
-    drs = rs_examples.drs_mutex(N)
+    # Distributed RS:
+    #drs = rs_examples.drs_mutex(N)
     #drs.show()
 
-    smt = SmtCheckerDistribRS(drs,debug_level=0)
+    #smt = SmtCheckerDistribRS(drs,debug_level=0)
-    smt.check_reachability(rs_examples.drs_mutex_property1(N),
+    #smt.check_reachability(rs_examples.drs_mutex_property1(N),
-        exclusive_state=False,
+    #    exclusive_state=False,
-        max_level=10,
+    #    max_level=10,
-        print_time=True,
+    #    print_time=True,
-        print_mem=True)
+    #    print_mem=True)
 
     # drs = rs_examples.drs_toy_ex1()
     # drs.show()