working on the encoding for rsLTL, testing functionality

logics/__init__.py

@@ -1,2 +1,3 @@
 from logics.rsltl import Formula_rsLTL
 from logics.rsltl import BagDescription
+from logics.rsltl import Encoder_rsLTL

logics/rsltl.py

@@ -133,7 +133,6 @@ class Formula_rsLTL(object):
         return Formula_rsLTL(rsLTL_form_type.l_not, L_oper = self)
 
 
-
 class Encoder_rsLTL(object):
     """Class for encoding rsLTL formulae for a given smt_checker instance"""
         
@@ -145,7 +144,7 @@ class Encoder_rsLTL(object):
         
     def encode_bag(self, bag_formula, level, context=False):
         if bag_formula.f_type == BagDesc_oper.entity:
-            entity_id = self.rs.get_entity_id(self.entity)
+            entity_id = self.rs.get_entity_id(bag_formula.entity)
             if context:
                 return self.v_ctx[level][entity_id]
             else:

rs/reaction_system_with_concentrations.py

@@ -23,7 +23,7 @@ class ReactionSystemWithConcentrations(ReactionSystem):
             name,def_max_conc = e
         elif type(e) is str:
             name = e
-            print("\n\nWARNING: no maximal concentration level specified for:", e, "\n\n")
+            print("\nWARNING: no maximal concentration level specified for:", e, "\n")
         else:
             raise RuntimeError("Bad entity type when adding background set element")
 

rs_testing.py

@@ -1,11 +1,39 @@
 from rs import *
 from smt import *
 import rs_examples 
+from logics import *
 
 def run_tests():
     
-    test_extended_automaton()
+    # test_extended_automaton()
     # process()
+    test_rsLTL()
+    
+def test_rsLTL():
+
+    r = ReactionSystemWithConcentrations()
+    r.add_bg_set_entity(("a",2))
+    r.add_bg_set_entity(("inc",2))
+    r.add_bg_set_entity(("dec",2))
+    r.add_bg_set_entity(("ent1",5))
+    r.add_bg_set_entity(("ent2",3))
+    r.add_bg_set_entity(("ent3",3))
+
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("init")
+    c.add_state("working")
+    c.add_transition("init", [("a",1),("inc",1)], "working")
+    c.add_transition("working", [("inc",1)], "working")
+
+    x = ( Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_bag( ~((BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) ) ) ) & Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_bag( ~((BagDescription.f_entity("ent3") == 1) ) ) )
+    print(x)
+    
+    rc = ReactionSystemWithAutomaton(r,c)
+    checker = SmtCheckerRSC(rc)
+    checker.dummy_unroll(10)
+    e = Encoder_rsLTL(checker)
+    
+    print(e.encode(x, 1, 10))
 
 def test_extended_automaton():
     

smt/smt_checker_rsc.py

@@ -368,10 +368,13 @@ class SmtCheckerRSC(object):
     def check_rsltl(self, formula, print_witness=True):
         """Bounded Model Checking for rsLTL properties"""
         
+    def dummy_unroll(self, levels):
         
+        for i in range(levels):
+            self.prepare_all_variables()
 
     def check_reachability(self, state, print_witness=True, 
-            print_time=True, print_mem=True, max_level=100):
+            print_time=True, print_mem=True, max_level=1000):
         """Main testing function"""
 
         if print_time: