From 9e0ca1d654bdc73e54362170f6bcc4aca49da59d Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Fri, 22 Feb 2019 23:14:57 +0000
Subject: [PATCH] Example: overview

---
 doc/overview.py | 44 +++++++++++++++++++++++++++
 phd_example.py  | 79 -------------------------------------------------
 2 files changed, 44 insertions(+), 79 deletions(-)
 create mode 100755 doc/overview.py
 delete mode 100755 phd_example.py

diff --git a/doc/overview.py b/doc/overview.py
new file mode 100755
index 0000000..5fe094b
--- /dev/null
+++ b/doc/overview.py
@@ -0,0 +1,44 @@
+#!/usr/bin/env python
+
+from rs import *
+from smt import *
+from logics import *
+from rsltl_shortcuts import *
+
+def ex():
+    
+    prs = ReactionSystemWithConcentrationsParam()
+    
+    ent_with_conc = [("a", 3), ("b",2), ("c",1), ("h",1)]
+
+    for ec in ent_with_conc:
+        prs.add_bg_set_entity(ec)
+
+    lda = prs.get_param("lda")
+    
+    prs.add_reaction([("a",1)],[("h",1)],[("b", 2)])
+    prs.add_reaction(lda,[("h",1)],[("c",1)])
+    
+    ##
+
+    ca = ContextAutomatonWithConcentrations(prs)
+    ca.add_init_state("0")
+    ca.add_state("1")
+    
+    ca.add_transition("0", [("a", 3)], "1")
+    ca.add_transition("1", [], "1")
+    ca.add_transition("1", [("h", 1)], "1")
+
+    crprs = ReactionSystemWithAutomaton(prs, ca)
+    crprs.show()
+
+    pc = param_entity(lda, "a") == 0
+    f = ltl_F(bag_entity("h") == 0, "c")
+
+    checker = SmtCheckerRSCParam(crprs, optimise=True)
+    checker.check_rsltl(formulae_list=[f], param_constr=pc)
+    
+if __name__ == "__main__":
+	ex()
+
+# EOF
diff --git a/phd_example.py b/phd_example.py
deleted file mode 100755
index 75b2ca6..0000000
--- a/phd_example.py
+++ /dev/null
@@ -1,79 +0,0 @@
-#!/usr/bin/env python
-
-from rs import *
-from smt import *
-from logics import *
-from rsltl_shortcuts import *
-
-def gen_expr():
-    
-    prs = ReactionSystemWithConcentrationsParam()
-    
-    ent_with_conc = [("a", 3), ("b",2), ("c",1), ("h",1)]
-
-    for ec in ent_with_conc:
-        prs.add_bg_set_entity(ec)
-
-    lda = prs.get_param("lda")
-    
-    prs.add_reaction([("a",1)],[("h",1)],[("b", 2)])
-    prs.add_reaction(lda,[("h",1)],[("c",1)])
-    
-    ##
-
-    ca = ContextAutomatonWithConcentrations(prs)
-    ca.add_init_state("0")
-    ca.add_state("1")
-    
-    ca.add_transition("0", [("a", 3)], "1")
-    ca.add_transition("1", [], "1")
-    ca.add_transition("1", [("h", 1)], "1")
-
-    crprs = ReactionSystemWithAutomaton(prs, ca)
-    crprs.show()
-
-    print("......")
-    
-    # cprs is defined in the SMT checker    
-
-    # reach_y = ltl_F(bag_entity("h") == 0, "y")
-    # reach_yp = ltl_F(bag_entity("h") == 0, "yp")
-    # reach_Y = ltl_F(bag_entity("h") == 0, "Y")
-    #
-
-
-    # # rules
-    # phi_c1 = ltl_G(bag_entity("h") == 0, ltl_Implies(
-    #     bag_entity("y") > 0,
-    #     ltl_X(True, bag_And(bag_entity("y") > 0, bag_entity("yp") > 0))))
-    #
-    # phi_c2 = ltl_G(bag_entity("h") == 0, ltl_Implies(
-    #     bag_And(bag_entity("y") > 0, bag_entity("yp") > 0),
-    #     ltl_F(True, bag_entity("Y") > 0)))
-    #
-    # # delayed_Y = ltl_X(True, ltl_And(bag_entity("Y") == 0, ltl_X(True, bag_entity("Y") == 0)))
-    #
-    # # delayed_Y = ltl_X(True, bag_entity("Y") == 0)
-    #
-    # delayed_Q = ltl_And(bag_entity("Q") == 0, ltl_X(True, ltl_And(bag_entity("Q") == 0, ltl_X(True, ltl_And(bag_entity("Q") == 0, ltl_F(True, bag_entity("Q") > 0))))))
-    #
-    # obs_1 = ltl_And(phi_r, phi_c1, phi_c2, delayed_Q)
-    
-    # obs_2 = ltl_And(f_y2, reach_y, reach_Y, delayed_Y, delayed_Q)
-
-    # f_x2 = ltl_G(True, ltl_Implies(
-    #     exact_state(["x", "xp"], all_entities),
-    #     ltl_X(bag_Not("h"), exact_state("X", all_entities))))
-    #
-    
-    pc = param_entity(lda, "a") == 0
-    f = ltl_F(bag_entity("h") == 0, "c")
-
-    checker = SmtCheckerRSCParam(crprs, optimise=True)
-    checker.check_rsltl(formulae_list=[f], param_constr=pc)
-    
-
-gen_expr()
-
-
-