From 827568e1740fc846660ad4e1b878b7619f8174a4 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur@Arturs-MacBook-Pro.local>
Date: Sun, 5 Mar 2017 12:58:24 +0100
Subject: [PATCH] working on the encoding for rsLTL, testing functionality

---
 logics/__init__.py                        |  1 +
 logics/rsltl.py                           |  3 +--
 rs/reaction_system_with_concentrations.py |  2 +-
 rs_testing.py                             | 30 ++++++++++++++++++++++-
 smt/smt_checker_rsc.py                    |  5 +++-
 5 files changed, 36 insertions(+), 5 deletions(-)

diff --git a/logics/__init__.py b/logics/__init__.py
index 9579ea8..848d5c1 100644
--- a/logics/__init__.py
+++ b/logics/__init__.py
@@ -1,2 +1,3 @@
 from logics.rsltl import Formula_rsLTL
 from logics.rsltl import BagDescription
+from logics.rsltl import Encoder_rsLTL
\ No newline at end of file
diff --git a/logics/rsltl.py b/logics/rsltl.py
index 5873e2a..9f41366 100644
--- a/logics/rsltl.py
+++ b/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:
diff --git a/rs/reaction_system_with_concentrations.py b/rs/reaction_system_with_concentrations.py
index c8640ba..4167aa2 100644
--- a/rs/reaction_system_with_concentrations.py
+++ b/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")
 
diff --git a/rs_testing.py b/rs_testing.py
index 844a0e8..2cb3809 100644
--- a/rs_testing.py
+++ b/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():
     
diff --git a/smt/smt_checker_rsc.py b/smt/smt_checker_rsc.py
index 16f83b0..a2eadc7 100644
--- a/smt/smt_checker_rsc.py
+++ b/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: