Removing incorrect comment

LICENSE

@@ -0,0 +1,19 @@
+Copyright (c) 2015-2019 Artur Meski
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

README.md

@@ -3,6 +3,110 @@
 Reaction Systems Verification Toolkit
 
 The toolkit consists of two separate modules implementing:
-* BDD-based methods
-* SMT-based methods
+* Methods implemented using binary decision diagrams (BDD) for storing and manipulating the state space of the verified system.
+* Methods translating the verification problems into satisfiability modulo theories (SMT).
+
+# Installation
+
+## Installing everything manually
+
+(to be added)
+
+## Virtual Machine
+
+The easiest way to try out ReactICS is to download [the VM where everything is alread installed](http://reactionsystems.org/ReactICS.zip). This a VirtualBox virtual machine. After booting it up, you can log in as `reactics` with the same password. After logging in, ReactICS is available in the `reactics` directory:
+
+```
+$ cd reactics
+```
+
+An update and setup needs to be performed before running any type of verification:
+
+```
+$ ./reactics setup
+```
+
+After performing these steps you should be ready to start using ReactICS.
+
+## Examples
+
+The `examples` directory contains sample input files.
+
+### Multi-agent reaction systems (rsCTLK verification)
+
+To quickly test the BDD module you can perform verification of the TGC controller consiting of three trains:
+
+```
+$ ./reactics bdd -c f1 examples/bdd/tgc.rs
+```
+
+The above command tests the formula labelled `f1` in the input file.
+
+### Reachability
+
+To test the SMT module you can perform reachability verification of the scalable chain system:
+
+Running the benchmark without any arguments tells us what parameters are available:
+
+```
+$ ./reactics smt examples/smt/scalable_chain.py
+
+ ------------------------------------------------
+ -- ReactICS -- Reaction Systems Model Checker --
+ ------------------------------------------------
+
+arguments: <chainLen> <maxConc> <formulaNumber>
+```
+
+We may execute the benchmark for `chainLen=2`, `maxConc=3`, and `formulaNumber=1` using the following command:
+
+```
+$ ./reactics smt examples/smt/chain_reaction.py 2 3 1
+```
+
+### rsLTL verification
+
+To test the SMT module for rsLTL verification the scalable chain system benchmark may be used.
+
+
+
+```
+$ ./reactics smt examples/smt/scalable_chain.py 2 5 1
+```
+
+
+
+### Reaction synthesis
+
+To test the reaction synthesis approach on a mutual exclution protocol modelling three processes, run the following command (three processes, parametric verification, result optimised with OptSMT):
+
+```
+$ ./reactics smt examples/smt/mutex_param.py 3 p -o
+```
+
+To check the available parameters for the benchmark, we run it with `-h`:
+
+```
+$ ./reactics smt examples/smt/mutex_param.py -h
+
+ ------------------------------------------------
+ -- ReactICS -- Reaction Systems Model Checker --
+ ------------------------------------------------
+
+usage: mutex_param.py [-h] [-v] [-o] scaling {p,np-p,np-np}
+
+positional arguments:
+  scaling         scaling parameter value
+  {p,np-p,np-np}  Selects the mode: p - parameter synthesis (parametric
+                  implementation), np-p - non-parametric with parametric
+                  implementation (with the parameters substituted), np-np -
+                  non-parametric with non-parametric implementation
+                  (parameters substituted)
+
+optional arguments:
+  -h, --help      show this help message and exit
+  -v, --verbose   turn verbosity on
+  -o, --optimise  minimise the parametric computation result
+```
+
 

examples/bdd/generators/gen_tgc.py

@@ -0,0 +1,117 @@
+#!/usr/bin/env python
+
+from sys import argv,exit
+
+OPTIONS_STR = """
+options { use-context-automaton; make-progressive; };
+"""
+
+PROC_STR = """
+    proc{:d} {{
+        {{{{out}}, {{}} -> {{approach}}}};
+        {{{{approach}}, {{req}} -> {{req}}}};
+        {{{{allowed}}, {{}} -> {{in}}}};
+        {{{{in}}, {{}} -> {{out,leave}}}};
+        {{{{req}}, {{in}} -> {{req}}}};
+    }};
+"""
+
+CA_STR = """
+context-automaton {{
+    states {{ init, green, red }};
+    init-state {{ init }};
+    transitions {{
+{:s}
+    }};
+}};
+"""
+
+PROPERTY_STR = """
+rsctlk-property {{ {:s} : {:s} }};
+"""
+
+
+#################################################################
+
+if len(argv) < 1:
+    print("Usage: {:s} <number of processes>".format(argv[0]))
+    exit(100)
+
+n = int(argv[1])
+
+assert n > 1, "number of proc must be > 1"
+
+out = ""
+
+out += OPTIONS_STR
+out += "reactions {\n"
+for i in range(n):
+    out += PROC_STR.format(i)
+out += "};\n"
+
+transitions = ""
+
+init_trans = 8*" " + "{ "
+for i in range(n):
+    init_trans += "proc{:d}={{out}} ".format(i)
+init_trans += "}: init -> green;\n"
+transitions += init_trans
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{allowed}} }}: green -> red : proc{:d}.req;\n".format(8*" ", i, i)
+
+no_req_cond = "~proc0.req"
+for i in range(1, n):
+     no_req_cond += " AND ~proc{:d}.req".format(i)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: green -> green : {:s};\n".format(8*" ", i, no_req_cond)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: red -> green : proc{:d}.leave;\n".format(8*" ", i, i)
+
+no_leave_cond = "~proc0.leave"
+for i in range(1, n):
+     no_leave_cond += " AND ~proc{:d}.leave".format(i)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: red -> red : {:s};\n".format(8*" ", i, no_leave_cond)
+
+out += CA_STR.format(transitions)
+
+## f1
+#formula = "EF( proc0.in )"
+#out += PROPERTY_STR.format("f1",formula)
+
+# f1
+formula = "EF( E<proc0.allowed>X( proc0.in ) )"
+for i in range(1, n):
+    formula += " AND EF( E<proc{:d}.allowed>X( proc{:d}.in ) )".format(i, i)
+out += PROPERTY_STR.format("f1",formula)
+
+# f2
+formula = "EF( proc0.approach"
+for i in range(1, n):
+    formula += " AND proc{:d}.approach".format(i)
+formula += " )"
+out += PROPERTY_STR.format("f2",formula)
+
+# f3
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
+out += PROPERTY_STR.format("f3",formula)
+
+# f4
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+all_agents = "proc0"
+for i in range(1, n):
+    all_agents += ",proc{:d}".format(i)
+formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents,subf)
+out += PROPERTY_STR.format("f4",formula)
+
+print(out)
+

examples/bdd/tgc.rs

@@ -0,0 +1,58 @@
+
+options { use-context-automaton; make-progressive; };
+reactions {
+
+    proc0 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+
+    proc1 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+
+    proc2 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+};
+
+context-automaton {
+    states { init, green, red };
+    init-state { init };
+    transitions {
+        { proc0={out} proc1={out} proc2={out} }: init -> green;
+        { proc0={allowed} }: green -> red : proc0.req;
+        { proc1={allowed} }: green -> red : proc1.req;
+        { proc2={allowed} }: green -> red : proc2.req;
+        { proc0={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc1={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc2={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc0={} }: red -> green : proc0.leave;
+        { proc1={} }: red -> green : proc1.leave;
+        { proc2={} }: red -> green : proc2.leave;
+        { proc0={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+        { proc1={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+        { proc2={} }: red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+
+    };
+};
+
+rsctlk-property { f1 : EF( E<proc0.allowed>X( proc0.in ) ) AND EF( E<proc1.allowed>X( proc1.in ) ) AND EF( E<proc2.allowed>X( proc2.in ) ) };
+
+rsctlk-property { f2 : EF( proc0.approach AND proc1.approach AND proc2.approach ) };
+
+rsctlk-property { f3 : AG( proc0.in IMPLIES K[proc0](~proc1.in AND ~proc2.in) ) };
+
+rsctlk-property { f4 : AG( proc0.in IMPLIES C[proc0,proc1,proc2](~proc1.in AND ~proc2.in) ) };
+

examples/smt/chain_reaction.py

@@ -0,0 +1,125 @@
+#!/usr/bin/env python
+#
+# Copyright (c) 2015-2019 Artur Meski
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+#
+
+from rs import *
+from smt import *
+import sys
+import resource
+
+
+def chain_reaction(print_system=False):
+
+    if len(sys.argv) < 1 + 3:
+        print("{source} <N> <M> <type>".format(source=sys.argv[0]))
+        print()
+        print("* N,M -- integers (scaling parameters)")
+        print("* type:")
+        print("  - 1 - RSC")
+        print("  - 0 - RSC translated into RS")
+        print()
+        exit(1)
+
+    chainLen = int(sys.argv[1])  
+    maxConc = int(sys.argv[2])  # depth (max concentration)
+
+    verify_rsc = bool(int(sys.argv[3]))
+
+    if chainLen < 1 or maxConc < 1:
+        print("be reasonable")
+        exit(1)
+
+    r = ReactionSystemWithConcentrations()
+    r.add_bg_set_entity(("inc", 1))
+    r.add_bg_set_entity(("dec", 1))
+
+    for i in range(1, chainLen + 1):
+        r.add_bg_set_entity(("e_" + str(i), maxConc))
+
+    for i in range(1, chainLen + 1):
+        ent = "e_" + str(i)
+        r.add_reaction_inc(ent, "inc", [(ent, 1)], [(ent, maxConc)])
+        r.add_reaction_dec(ent, "dec", [(ent, 1)], [])
+        if i < chainLen:
+            r.add_reaction([(ent, maxConc)], [], [("e_" + str(i + 1), 1)])
+
+    r.add_reaction(
+        [("e_" + str(chainLen), maxConc)],
+        [("dec", 1)],
+        [("e_" + str(chainLen), maxConc)],
+    )
+
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("init")
+    c.add_state("working")
+    c.add_transition("init", [("e_1", 1), ("inc", 1)], "working")
+    c.add_transition("working", [("inc", 1)], "working")
+
+    rc = ReactionSystemWithAutomaton(r, c)
+
+    if print_system:
+        rc.show()
+
+    if verify_rsc:
+        smt_rsc = SmtCheckerRSC(rc)
+        prop = [("e_" + str(chainLen), maxConc)]
+        smt_rsc.check_reachability((prop, []), max_level=maxConc * chainLen + 10)
+
+    else:
+        orc = rc.get_ordinary_reaction_system_with_automaton()
+        if print_system:
+            print("\nTranslated:")
+            orc.show()
+        smt_tr_rs = SmtCheckerRS(orc)
+        smt_tr_rs.check_reachability(["e_" + str(chainLen) + "#" + str(maxConc)])
+
+    time = 0
+    mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+    if verify_rsc:
+        filename_t = "bench_rsc_time.log"
+        filename_m = "bench_rsc_mem.log"
+        time = smt_rsc.get_verification_time()
+    else:
+        filename_t = "bench_tr_rs_time.log"
+        filename_m = "bench_tr_rs_mem.log"
+        time = smt_tr_rs.get_verification_time()
+
+    f = open(filename_t, "a")
+    log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n"
+    f.write(log_str)
+    f.close()
+
+    f = open(filename_m, "a")
+    log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n"
+    f.write(log_str)
+    f.close()
+
+
+def main():
+
+    chain_reaction()
+
+
+if __name__ == "__main__":
+    main()
+
+# EOF

examples/smt/heat_shock_response.py

@@ -1,106 +1,40 @@
 #!/usr/bin/env python
+#
+# Copyright (c) 2015-2019 Artur Meski
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+#
 
 from rs import *
 from smt import *
 import sys
 import resource
 
-def chain_reaction(print_system=False):
 
-    if len(sys.argv) < 1+3:
-        print("provide N M B")
-        print(" B=1 - RSC")
-        print(" B=0 - Translated RSC into RS")
-        exit(1)
-
-    chainLen=int(sys.argv[1]) # chain length
-    maxConc=int(sys.argv[2]) # depth (max concentration)
-    verify_rsc=bool(int(sys.argv[3]))
-        
-    if chainLen < 1 or maxConc < 1:
-        print("be reasonable")
-        exit(1)
-    
-    r = ReactionSystemWithConcentrations()
-    r.add_bg_set_entity(("inc",1))
-    # r.add_bg_set_entity(("reset",1))
-    r.add_bg_set_entity(("dec",1))
-    # r.add_bg_set_entity(("x",1))
-    
-    for i in range(1,chainLen+1):
-        r.add_bg_set_entity(("e_" + str(i),maxConc))
-    
-    for i in range(1,chainLen+1):
-        ent = "e_" + str(i)
-        # r.add_reaction_inc(ent, "inc", [(ent, 1)],[("reset",1),(ent,maxConc)])
-        r.add_reaction_inc(ent, "inc", [(ent, 1)],[(ent,maxConc)])
-        r.add_reaction_dec(ent, "dec", [(ent, 1)],[])
-        # r.add_reaction([(ent,1),("reset",1)],[],[(ent,1)])
-        if i < chainLen:
-            r.add_reaction([(ent,maxConc)],[],[("e_"+str(i+1),1)])
-
-    r.add_reaction([("e_" + str(chainLen),maxConc)],[("dec",1)],[("e_" + str(chainLen),maxConc)])
-    # r.add_reaction([("e_" + str(chainLen),maxConc)],[],[("e_" + str(chainLen),maxConc)])
-    
-    
-    c = ContextAutomatonWithConcentrations(r)
-    c.add_init_state("init")
-    c.add_state("working")
-    c.add_transition("init", [("e_1",1),("inc",1)], "working")
-    c.add_transition("working", [("inc",1)], "working")
-    # c.add_transition("working", [("reset",1)], "working")
-    # c.add_transition("working",[("x",1)],"working")
-
-    rc = ReactionSystemWithAutomaton(r,c)
-    
-    if print_system:
-        rc.show()
-    
-    if verify_rsc:
-        smt_rsc = SmtCheckerRSC(rc)
-        prop = [('e_'+str(chainLen),maxConc)]
-        smt_rsc.check_reachability((prop,[]),max_level=maxConc*chainLen+10)
-        # smt_rsc.show_encoding(prop,print_time=True,max_level=maxConc*chainLen+10)
-
-    else:
-        orc = rc.get_ordinary_reaction_system_with_automaton()
-        if print_system:
-            print("\nTranslated:")
-            orc.show()
-        smt_tr_rs = SmtCheckerRS(orc)
-        smt_tr_rs.check_reachability(['e_'+str(chainLen)+"#"+str(maxConc)])
-    
-    # print("Reaction System with Concentrations:", smt_rsc.get_verification_time())
-    # print("Reaction System from translating RSC:", smt_tr_rs.get_verification_time())
-    
-    time=0
-    mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)
-    if verify_rsc:
-        filename_t="bench_rsc_time.log"
-        filename_m="bench_rsc_mem.log"
-        time=smt_rsc.get_verification_time()
-    else:
-        filename_t="bench_tr_rs_time.log"
-        filename_m="bench_tr_rs_mem.log"
-        time=smt_tr_rs.get_verification_time()
-
-    f=open(filename_t, 'a')    
-    log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n"
-    f.write(log_str)
-    f.close()
-    
-    f=open(filename_m, 'a')
-    log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n"
-    f.write(log_str)
-    f.close()
-
-
-def heat_shock_response(print_system=True,verify_rsc=True):
+def heat_shock_response(print_system=True, verify_rsc=True):
 
     if len(sys.argv) < 1+1:
-        print("provide B")
-        print(" B=1 - RSC")
-        print(" B=0 - Translated RSC into RS")
+        print("{source} <type>".format(source=sys.argv[0]))
+        print("type:")
+        print(" - 1 -- RSC")
+        print(" - 0 -- RSC translated into RS")
+        print()
         exit(1)
 
     verify_rsc=bool(int(sys.argv[1]))
@@ -147,27 +81,20 @@ def heat_shock_response(print_system=True,verify_rsc=True):
     r.add_reaction_dec("temp", "cool", [("temp",1)],[])
 
     r.add_permanency("temp",[("heat",1),("cool",1)])
-    #r.add_permanency("temp",[])
 
     c = ContextAutomatonWithConcentrations(r)
     c.add_init_state("0")
     c.add_state("1")
-    # c.add_transition("0", [("prot",1), ("temp",35)], "1")
     c.add_transition("0", [("hsf",1),("prot",1),("hse",1),("temp",35)], "1")
-    #-> c.add_transition("0", [("hse",1),("prot",1),("hsp:hsf",1),("temp",stress_temp)], "1")
-    # c.add_transition("0", [("hsp",1),("prot",1),("hsf3:hse",1),("mfp",1),("hsp:mfp",1),("temp",30)], "1")
     c.add_transition("1", [("cool",1)], "1")
     c.add_transition("1", [("heat",1)], "1")
     c.add_transition("1", [], "1")
-    # c.add_transition("1", [("sugar",1)], "1")
 
     rc = ReactionSystemWithAutomaton(r,c)
     
     if print_system:
         rc.show()
     
-    # prop_req = [("hsp:hsf",1),("hse",1),("prot",1)]
-    # prop_block = [("temp",stress_temp)]
     prop_req   = [ ("mfp",1) ]
     prop_block = [ ]
     prop       = (prop_req,prop_block)
@@ -184,7 +111,16 @@ def heat_shock_response(print_system=True,verify_rsc=True):
         smt_tr_rs = SmtCheckerRS(orc)
         smt_tr_rs.check_reachability(rs_prop)
 
+
 def state_translate_rsc2rs(p):
     return [e[0] + "#" + str(e[1]) for e in p]
 
+
+def main():
+
+    heat_shock_response()
+
+if __name__ == "__main__":
+    main()
+        
 # EOF

examples/smt/mutex_param.py

@@ -0,0 +1,457 @@
+#
+# Copyright (c) 2015-2019 Artur Meski
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+#
+
+from rs import *
+from smt import *
+from logics import *
+from rsltl_shortcuts import *
+
+from itertools import chain, combinations
+
+import sys
+import resource
+import argparse
+
+
+def powerset(iterable, N=None):
+    if N is None:
+        N = len(s)
+    s = list(iterable)
+    return chain.from_iterable(combinations(s, r) for r in range(N + 1))
+
+
+def mutex_param_bench(cmd_args):
+    """
+    Mutex Benchmark
+    
+    Parametric
+    """
+
+    base_entities = ["out", "req", "in", "act"]
+    shared_entities = ["lock", "done", "s"]
+
+    if not cmd_args.scaling:
+        print("Missing scaling parameter")
+        return
+    n_proc = int(cmd_args.scaling)
+
+    r = ReactionSystemWithConcentrationsParam()
+
+    def E(a, b, c=1):
+        return (a + "_" + str(b), c)
+
+    for i in range(n_proc):
+        for ent in base_entities:
+            max_conc = 1
+            if ent == "in":
+                max_conc = 3
+            elif ent == "req":
+                max_conc = 2
+            r.add_bg_set_entity(E(ent, i, max_conc))
+
+    for ent in shared_entities:
+        max_conc = 1
+        r.add_bg_set_entity((ent, max_conc))
+
+    ###################################################
+
+    Inhib = [("s", 1)]
+
+    for i in range(n_proc):
+
+        r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
+        r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
+
+        for j in range(n_proc):
+            if i != j:
+                r.add_reaction(
+                    [E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
+                )
+
+        r.add_reaction([E("req", i)], [E("act", i)], [E("req", i, 2)])
+
+        enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
+        r.add_reaction(
+            [E("req", i, 2), E("act", i)], enter_inhib, [E("in", i, 3), ("lock", 1)]
+        )
+
+        r.add_reaction([E("in", i, 3), E("act", i)], Inhib, [E("in", i, 2)])
+        r.add_reaction([E("in", i, 2), E("act", i)], Inhib, [E("in", i, 1)])
+
+        r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
+        r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
+
+    r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
+
+    lda1 = r.get_param("lda1")
+    lda2 = r.get_param("lda2")
+    lda3 = r.get_param("lda3")
+
+    r.add_reaction(lda1, lda2, lda3)
+
+    ###################################################
+
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("0")
+    c.add_state("1")
+
+    init_ctx = []
+    for i in range(n_proc):
+        init_ctx.append(E("out", i))
+
+    # the experiments starts with adding x and y:
+    c.add_transition("0", init_ctx, "1")
+
+    all_act = powerset([E("act", i) for i in range(n_proc)], 2)
+
+    for actions in all_act:
+        actions = list(actions)
+
+        c.add_transition("1", actions, "1")
+
+    # for all the remaining steps we have empty context sequences
+    # c.add_transition("1", [], "1")
+    # c.add_transition("1", [("h", 1)], "1")
+
+    ###################################################
+
+    rc = ReactionSystemWithAutomaton(r, c)
+    rc.show()
+
+    f_attack = ltl_F(
+        True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
+    )
+
+    ent_of_Nth_proc = [
+        ent + "_" + str(n_proc - 1) for ent in base_entities
+    ] + shared_entities
+    disallow = ["in_" + str(n_proc - 1)]
+    for ent in r.background_set:
+        if ent not in ent_of_Nth_proc:
+            disallow.append(ent)
+
+    # disallow.append("act_" + str(n_proc-1))
+
+    # disallow = ["in_0", "in_" + str(n_proc)] #, "req_0", "req_1"]
+    lda1_disallow = [param_entity(lda1, ent) == 0 for ent in disallow]
+    lda2_disallow = [param_entity(lda2, ent) == 0 for ent in disallow]
+    lda3_disallow = [param_entity(lda3, ent) == 0 for ent in disallow]
+    lda_disallow = lda1_disallow + lda2_disallow + lda3_disallow
+
+    # for bent in base_entities:
+    #     print(param_entity(lda3, bent + "_0"))
+
+    param_constr = param_And(*lda_disallow)
+
+    smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
+    smt_rsc.check_rsltl(
+        formulae_list=[f_attack], param_constr=param_constr
+    )  # , max_level=4, cont_if_sat=True)
+
+    log_suffix = ""
+    if cmd_args.optimise:
+        log_suffix = "_OPT"
+
+    time = 0
+    mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+    filename_t = "bench_mutex_param" + log_suffix + "_time.dat"
+    filename_m = "bench_mutex_param" + log_suffix + "_mem.dat"
+    time = smt_rsc.get_verification_time()
+
+    with open(filename_t, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, time)
+        f.write(log_str)
+
+    with open(filename_m, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
+        f.write(log_str)
+
+
+def mutex_nonparam_bench(cmd_args):
+    """
+    Mutex Benchmark
+    
+    Parametric
+    """
+
+    base_entities = ["out", "req", "in", "act"]
+    shared_entities = ["lock", "done", "s"]
+
+    if not cmd_args.scaling:
+        raise RuntimeError("Missing scaling parameter")
+    n_proc = int(cmd_args.scaling)
+
+    r = ReactionSystemWithConcentrationsParam()
+
+    def E(a, b):
+        return (a + "_" + str(b), 1)
+
+    for i in range(n_proc):
+        for ent in base_entities:
+            r.add_bg_set_entity(E(ent, i))
+
+    for ent in shared_entities:
+        r.add_bg_set_entity((ent, 1))
+
+    ###################################################
+
+    Inhib = [("s", 1)]
+
+    for i in range(n_proc):
+
+        r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
+        r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
+
+        for j in range(n_proc):
+            if i != j:
+                r.add_reaction(
+                    [E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
+                )
+
+        r.add_reaction([E("req", i)], [E("act", i)], [E("req", i)])
+
+        enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
+        r.add_reaction(
+            [E("req", i), E("act", i)], enter_inhib, [E("in", i), ("lock", 1)]
+        )
+
+        r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
+        r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
+
+    r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
+
+    r.add_reaction(
+        [E("out", n_proc - 1)], [("s", 1)], [("done", 1), E("req", n_proc - 1)]
+    )
+
+    ###################################################
+
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("0")
+    c.add_state("1")
+
+    init_ctx = []
+    for i in range(n_proc):
+        init_ctx.append(E("out", i))
+
+    # the experiments starts with adding x and y:
+    c.add_transition("0", init_ctx, "1")
+
+    all_act = powerset([E("act", i) for i in range(n_proc)], 2)
+
+    for actions in all_act:
+        actions = list(actions)
+
+        c.add_transition("1", actions, "1")
+
+    # for all the remaining steps we have empty context sequences
+    # c.add_transition("1", [], "1")
+    # c.add_transition("1", [("h", 1)], "1")
+
+    ###################################################
+
+    rc = ReactionSystemWithAutomaton(r, c)
+    rc.show()
+
+    f_attack = ltl_F(
+        True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
+    )
+
+    smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
+    smt_rsc.check_rsltl(formulae_list=[f_attack])
+
+    time = 0
+    mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+    filename_t = "bench_mutex_nonparam_time.dat"
+    filename_m = "bench_mutex_nonparam_mem.dat"
+    time = smt_rsc.get_verification_time()
+
+    with open(filename_t, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, time)
+        f.write(log_str)
+
+    with open(filename_m, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
+        f.write(log_str)
+
+
+def mutex_nonparam_bench_oldimpl(cmd_args):
+    """
+    Mutex Benchmark
+    
+    Parametric
+    """
+
+    base_entities = ["out", "req", "in", "act"]
+    shared_entities = ["lock", "done", "s"]
+
+    if not cmd_args.scaling:
+        raise RuntimeError("Missing scaling parameter")
+    n_proc = int(cmd_args.scaling)
+
+    r = ReactionSystemWithConcentrations()
+
+    def E(a, b):
+        return (a + "_" + str(b), 1)
+
+    for i in range(n_proc):
+        for ent in base_entities:
+            r.add_bg_set_entity(E(ent, i))
+
+    for ent in shared_entities:
+        r.add_bg_set_entity((ent, 1))
+
+    ###################################################
+
+    Inhib = [("s", 1)]
+
+    for i in range(n_proc):
+
+        r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
+        r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
+
+        for j in range(n_proc):
+            if i != j:
+                r.add_reaction(
+                    [E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
+                )
+
+        r.add_reaction([E("req", i)], [E("act", i)], [E("req", i)])
+
+        enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
+        r.add_reaction(
+            [E("req", i), E("act", i)], enter_inhib, [E("in", i), ("lock", 1)]
+        )
+
+        r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
+        r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
+
+    r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
+
+    r.add_reaction(
+        [E("out", n_proc - 1)], [("s", 1)], [("done", 1), E("req", n_proc - 1)]
+    )
+
+    ###################################################
+
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("0")
+    c.add_state("1")
+
+    init_ctx = []
+    for i in range(n_proc):
+        init_ctx.append(E("out", i))
+
+    # the experiments starts with adding x and y:
+    c.add_transition("0", init_ctx, "1")
+
+    all_act = powerset([E("act", i) for i in range(n_proc)], 2)
+
+    for actions in all_act:
+        actions = list(actions)
+
+        c.add_transition("1", actions, "1")
+
+    # for all the remaining steps we have empty context sequences
+    # c.add_transition("1", [], "1")
+    # c.add_transition("1", [("h", 1)], "1")
+
+    ###################################################
+
+    rc = ReactionSystemWithAutomaton(r, c)
+    rc.show()
+
+    f_attack = ltl_F(
+        True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
+    )
+
+    smt_rsc = SmtCheckerRSC(rc)
+    smt_rsc.check_rsltl(formula=f_attack)
+
+    time = 0
+    mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+    filename_t = "bench_mutex_nonparam_oldimpl_time.dat"
+    filename_m = "bench_mutex_nonparam_oldimpl_mem.dat"
+    time = smt_rsc.get_verification_time()
+
+    with open(filename_t, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, time)
+        f.write(log_str)
+
+    with open(filename_m, "a") as f:
+        log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
+        f.write(log_str)
+
+
+def state_translate_rsc2rs(p):
+    return [e[0] + "#" + str(e[1]) for e in p]
+
+
+def mutex_bench_main(cmd_args):
+
+    mode = cmd_args.mode
+
+    if mode == "p":
+        mutex_param_bench(cmd_args)
+    elif mode == "np-p":
+        mutex_nonparam_bench(cmd_args)
+    elif mode == "np-np":
+        mutex_nonparam_bench_oldimpl(cmd_args)
+    else:
+        print("Unrecognised mode")
+        return
+
+
+def main():
+
+    parser = argparse.ArgumentParser()
+
+    parser.add_argument(
+        "scaling",
+        help="scaling parameter value",
+    )
+    
+    parser.add_argument(
+        "mode",
+        choices=['p', 'np-p', 'np-np'], 
+        help="Selects the mode: p - parameter synthesis (parametric implementation), np-p - non-parametric with parametric implementation (with the parameters substituted), np-np - non-parametric with non-parametric implementation (parameters substituted)",
+    )
+
+    parser.add_argument(
+        "-v", "--verbose", help="turn verbosity on", action="store_true"
+    )
+    parser.add_argument(
+        "-o",
+        "--optimise",
+        help="minimise the parametric computation result",
+        action="store_true",
+    )
+
+    args = parser.parse_args()
+        
+    mutex_bench_main(args)
+
+
+if __name__ == "__main__":
+    main()
+
+# EOF

examples/smt/scalable_chain.py

@@ -0,0 +1,173 @@
+#!/usr/bin/env python
+#
+# Copyright (c) 2015-2019 Artur Meski
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+#
+
+from rs import *
+from smt import *
+from logics import *
+from rsltl_shortcuts import *
+
+from itertools import chain, combinations
+
+import sys
+import resource
+
+def generate_system(chainLen, maxConc):
+    """
+    This function generates the reaction system with concentrations
+    for the scalable chain benchmark
+    
+    chainLen is the length of the chain
+    maxConc is the maximal concentration
+    """
+    
+    r = ReactionSystemWithConcentrations()
+    r.add_bg_set_entity(("inc",1))
+    r.add_bg_set_entity(("dec",1))
+    
+    for i in range(1,chainLen+1):
+        r.add_bg_set_entity(("e_" + str(i),maxConc))
+    
+    for i in range(1,chainLen+1):
+        ent = "e_" + str(i)
+        r.add_reaction_inc(ent, "inc", [(ent, 1)],[(ent,maxConc)])
+        r.add_reaction_dec(ent, "dec", [(ent, 1)],[])
+        if i < chainLen:
+            r.add_reaction([(ent,maxConc)],[],[("e_"+str(i+1),1)])
+
+    r.add_reaction([("e_" + str(chainLen),maxConc)],[("dec",1)],[("e_" + str(chainLen),maxConc)])
+        
+    c = ContextAutomatonWithConcentrations(r)
+    c.add_init_state("init")
+    c.add_state("working")
+    c.add_transition("init", [("e_1",1),("inc",1)], "working")
+    c.add_transition("working", [("inc",1)], "working")
+    
+    rc = ReactionSystemWithAutomaton(r,c)
+
+    return rc
+
+def generate_formula(formula_number, chainLen, maxConc):
+    """
+    This function generates the rsLTL formula 
+    corresponding to the formula_number parameter
+    """
+
+    if formula_number == 1:
+        ret = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) >= maxConc) )
+
+    elif formula_number == 2:
+        f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) )
+        for i in range(chainLen-1,0,-1):
+            f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, f_tmp & (BagDescription.f_entity('e_'+str(i)) == maxConc) )
+        ret = f_tmp
+        
+    elif formula_number == 3:
+        ret = Formula_rsLTL.f_G( BagDescription.f_TRUE(),
+            Formula_rsLTL.f_Implies(
+                (BagDescription.f_entity('e_1') == 1),
+                Formula_rsLTL.f_F(
+                    BagDescription.f_entity("inc") > 0,
+                    (BagDescription.f_entity('e_'+str(chainLen)) == maxConc)
+                )
+            )
+        )
+
+    elif formula_number == 4:
+        ret = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') == maxConc )
+        
+    elif formula_number == 5:
+        ret = Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_U( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') > 0, BagDescription.f_entity('e_2') > 0 ) )
+
+    else:
+        ret = None
+        
+    assert ret is not None, "Unknown formula"
+
+    return ret
+
+
+def save_statistics(smt_rsc, formula_number, chainLen, maxConc):
+    """
+    Saves the statistics fetched from smt_rsc into files
+    """
+    time=0
+    mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)
+    filename_t="bench_rsc_F" + str(formula_number) + "_time.log"
+    filename_m="bench_rsc_F" + str(formula_number) + "_mem.log"
+    time=smt_rsc.get_verification_time()
+
+    f=open(filename_t, 'a')    
+    log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n"
+    f.write(log_str)
+    f.close()
+    
+    f=open(filename_m, 'a')
+    log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n"
+    f.write(log_str)
+    f.close()
+    
+
+def scalable_chain(print_system=False):
+    """
+    This is the entry point for the benchmark
+    """
+    if len(sys.argv) < 1+3:
+        print("arguments: <chainLen> <maxConc> <formulaNumber>")
+        exit(1)
+
+    chainLen=int(sys.argv[1]) # chain length
+    maxConc=int(sys.argv[2]) # depth (max concentration)
+    formula_number=int(sys.argv[3])
+        
+    if chainLen < 1 or maxConc < 1:
+        print("be reasonable")
+        exit(1)
+    if not formula_number in range(1,5+1):
+        print("formulaNumber must be in 1..5")
+        exit(1)
+    
+    # Generate the reaction systems with concentrations
+    rc = generate_system(chainLen, maxConc)
+    
+    # Generate the formula
+    form = generate_formula(formula_number, chainLen, maxConc)
+    
+    # Optional dump/print of the system
+    if print_system:
+        rc.show()
+    
+    # Create an instance of the SMT checker for RS with concentrations
+    smt_rsc = SmtCheckerRSC(rc)
+    
+    # Start the verification process
+    smt_rsc.check_rsltl(formula=form)
+        
+    save_statistics(smt_rsc, formula_number, chainLen, maxConc)
+        
+    
+def main():
+    scalable_chain(print_system=True)
+
+if __name__ == "__main__":
+    main()
+

reactics

@@ -0,0 +1,78 @@
+#!/bin/bash
+
+# 
+# Copyright (c) 2019 Artur Meski
+#
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+#
+# The above copyright notice and this permission notice shall be included in all
+# copies or substantial portions of the Software.
+#
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+# 
+
+echo
+echo " ------------------------------------------------"
+echo " -- ReactICS -- Reaction Systems Model Checker --"
+echo " ------------------------------------------------"
+echo
+
+mode="$1"
+shift
+
+REACTICS_BDD="$(pwd)/reactics-bdd"
+REACTICS_SMT="$(pwd)/reactics-smt"
+
+if [[ "$mode" == "bdd" ]]
+then
+  
+  if [[ ! -x $REACTICS_BDD/reactics ]]
+  then
+    echo "Make sure to run setup first!"
+  fi
+  
+  reactics-bdd/reactics $*
+  
+elif [[ "$mode" == "smt" ]]
+then
+ 
+  export PYTHONPATH="$PYTHONPATH:$REACTICS_SMT"
+  if [[ "$*" != "" ]]
+  then
+    python3 $* 
+  else
+    echo "Nothing to do"
+  fi
+  
+elif [[ "$mode" == "setup" ]]
+then
+ 
+  git pull 
+  cd $REACTICS_BDD
+  ./build_cudd.sh
+  make
+
+else
+  
+  echo "Usage: $0 <mode> <module-specific parameters>"
+  echo
+  echo "mode:"
+  echo "  - bdd    -- uses BDD-based module"
+  echo "  - smt    -- used SMT-based module"
+  echo "  - setup  -- builds what is required" 
+  echo
+  
+fi
+
+# EOF

reactics-bdd/formrsctlk.cc

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2012, 2013
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #include "formrsctlk.hh"

reactics-bdd/formrsctlk.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2012-2015
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef RS_FORMRSCTLK_HH

reactics-bdd/in/scripts/gen_asm.py

@@ -3,7 +3,7 @@
 from sys import argv,exit
 
 OPTIONS_STR = """
-options { use-context-automaton; make-progressive; }
+options { use-context-automaton; make-progressive; };
 """
 
 PROC_STR = """
@@ -25,16 +25,16 @@ FINAL_PROC = """
 
 CA_STR = """
 context-automaton {{
-    states {{ init, act }}
-    init-state {{ init }}
+    states {{ init, act }};
+    init-state {{ init }};
     transitions {{
 {:s}
-    }}
-}}
+    }};
+}};
 """
 
 PROPERTY_STR = """
-rsctlk-property {{ {:s} : {:s} }}
+rsctlk-property {{ {:s} : {:s} }};
 """
 
 
@@ -56,7 +56,7 @@ for i in range(1, n+1):
     out += PROC_STR.format(i)
 
 out += FINAL_PROC
-out += "}\n"
+out += "};\n"
 
 transitions = ""
 

reactics-bdd/in/scripts/gen_drs_mutex.py

@@ -1,89 +0,0 @@
-#!/usr/bin/env python
-
-from sys import argv,exit
-
-OPTIONS_STR = """
-options { use-context-automaton; }
-"""
-CONTROLLER_STR = """
-    ct {
-        {{lock},{leave} -> {lock}};
-        {{req},{} -> {lock}};
-    };
-"""
-
-PROC_STR = """
-    proc{:d} {{
-        {{{{out}}, {{}} -> {{approach}}}};
-        {{{{approach}}, {{req}} -> {{req}}}};
-        {{{{req}}, {{lock}} -> {{in}}}};
-        {{{{in}}, {{}} -> {{out,leave}}}};
-        {{{{req}}, {{in}} -> {{req}}}};
-    }};
-"""
-
-CA_STR = """
-context-automaton {{
-    states {{ s0, s1 }}
-    init-state {{ s0 }}
-    transitions {{
-{:s}
-    }}
-}}
-"""
-
-PROPERTY_STR = """
-rsctlk-property {{ {:s} : {:s} }}
-"""
-
-
-#################################################################
-
-if len(argv) < 1:
-    print("Usage: {:s} <number of processes>".format(argv[0]))
-    exit(100)
-
-n = int(argv[1])
-
-assert n > 1, "number of proc must be > 1"
-
-out = ""
-
-out += OPTIONS_STR
-out += "reactions {\n"
-out += CONTROLLER_STR
-for i in range(n):
-    out += PROC_STR.format(i)
-out += "}\n"
-
-transitions = ""
-
-init_trans = 8*" " + "{ ct={} "
-for i in range(n):
-    init_trans += "proc{:d}={{out}} ".format(i)
-
-init_trans += "}: s0 -> s1;\n"
-
-transitions += init_trans
-
-for i in range(n):
-    transitions += "{:s}{{ ct={{}} proc{:d}={{}} }}: s1 -> s1;\n".format(8*" ", i)    
-
-out += CA_STR.format(transitions)
-
-# f1
-formula = "EF( proc0.in )"
-for i in range(1, n):
-    formula += " AND EF( proc{:d}.in )".format(i)
-out += PROPERTY_STR.format("f1",formula)
-
-# f2
-subf = "~proc1.in"
-for i in range(2, n):
-    subf += " AND ~proc{:d}.in".format(i)
-formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
-
-out += PROPERTY_STR.format("f2",formula)
-
-print(out)
-

reactics-bdd/in/tgc.rs

@@ -1,48 +0,0 @@
-
-options { use-context-automaton; }
-reactions {
-
-    proc0 {
-        {{out}, {} -> {approach}};
-        {{approach}, {req} -> {req}};
-        {{allowed}, {} -> {in}};
-        {{in}, {} -> {out,leave}};
-        {{req}, {in} -> {req}};
-    };
-
-    proc1 {
-        {{out}, {} -> {approach}};
-        {{approach}, {req} -> {req}};
-        {{allowed}, {} -> {in}};
-        {{in}, {} -> {out,leave}};
-        {{req}, {in} -> {req}};
-    };
-
-    proc2 {
-        {{out}, {} -> {approach}};
-        {{approach}, {req} -> {req}};
-        {{allowed}, {} -> {in}};
-        {{in}, {} -> {out,leave}};
-        {{req}, {in} -> {req}};
-    };
-}
-
-context-automaton {
-    states { init, green, red }
-    init-state { init }
-    transitions {
-        { proc0={out} proc1={out} proc2={out} }: init -> green;
-        { proc0={} proc1={} proc2={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
-        { proc0={allowed} }: green -> red : proc0.req;
-        { proc1={allowed} }: green -> red : proc1.req;
-        { proc2={allowed} }: green -> red : proc2.req;
-        { proc0={} }: red -> green : proc0.leave;
-        { proc1={} }: red -> green : proc1.leave;
-        { proc2={} }: red -> green : proc2.leave;
-        { proc0={} proc1={} proc2={} } : red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
-    }
-}
-
-rsctlk-property { f1 : EF( proc0.in ) AND EF( proc1.in ) AND EF( proc2.in ) }
-
-rsctlk-property { f2 : AG( proc0.in IMPLIES K[proc0](~proc1.in AND ~proc2.in) ) }

reactics-bdd/in/trivial.rs

@@ -0,0 +1,22 @@
+options { use-context-automaton; };
+
+reactions {
+    m {
+        {{e1,e4},{e2} -> {e1,e2}}; 
+        {{e2},{e4} -> {e1,e3,e4}}; 
+	{{e1,e3},{e2} -> {e1,e2}};
+	{{e3},{e2} -> {e1}};
+    };
+
+};
+
+context-automaton {
+	states { s0, s1 };
+    init-state { s0 };
+	transitions {
+		{ m={e1,e4} }: s0 -> s1;
+		{ m={} }: s1 -> s1;
+		{ m={e4} }: s1 -> s1;
+	};
+};
+

reactics-bdd/memtime.hh

@@ -1,18 +1,3 @@
-/**************************************************************************
- *                                                                        *
- *  This file is a part of BMC4LTLK,                                      *
- *  a program for Bounded Model Checking of LTLK.                         *
- *                                                                        *
- *  Copyright (C) 2002-2010 Andrzej Zbrzezny <a.zbrzezny@gmail.com>       *
- *                                                                        *
- *  This program is released under the terms of the license contained     *
- *  in the file LICENSE.                                                  *
- *                                                                        *
- **************************************************************************/
-
-/* WARNING: LICENSE VIOLATION. THIS PROGRAM IS USED FOR TEST PURPOSES ONLY
- *          THIS CODE WILL BE REPLACED BEFORE ANY RELEASE!!!!
- */
 
 /* Based on MiniSat 1.14 */
 

reactics-bdd/reactics.cc

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2012-2014
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #include "reactics.hh"

reactics-bdd/rs.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2012-2014
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef RS_RS_HH

reactics-bdd/rsin_parser.yy

@@ -1,7 +1,7 @@
 %skeleton "lalr1.cc" /* -*- C++ -*- */
 %require "2.5"
 %defines
-%define parser_class_name {rsin_parser}
+%define api.parser.class {rsin_parser}
 
 %code requires {
 #include <string>
@@ -28,7 +28,7 @@ class rsin_driver;
 };
 
 %debug
-%error-verbose
+%define parse.error verbose
 
 // Symbols
 %union

reactics-bdd/stateconstr.cc

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #include "stateconstr.hh"

reactics-bdd/stateconstr.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef STATECONSTR_HH
@@ -11,6 +8,8 @@
 
 #include "types.hh"
 
+#include <cassert>
+
 /* For state constraints: */
 #define STC_PV   80
 #define STC_AND  81

reactics-bdd/symrs.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2012-2014
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef RS_SYMRSSTATE_HH

reactics-bdd/types.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef RS_TYPES_HH

reactics-smt/rs/reaction_system_with_concentrations_param.py

@@ -98,6 +98,24 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
         return False
 
+    def is_valid_concentration_for_entity(self, entity, level):
+        """Checks the concentration level for entity"""
+        e = self.get_entity_id(entity)
+        try:
+            max_conc = self.max_conc_per_ent[e]
+        except KeyError as _:
+            return True
+
+        if level > max_conc:
+            return False
+
+        return True
+
+    def terminate_on_invalid_concentration(self, entity, level):
+        if not self.is_valid_concentration_for_entity(entity, level):
+            print("FATAL. Invalid entity concentration: {:s}={:d}".format(entity, level))
+            exit(1)
+            
     def get_state_ids(self, state):
         """Returns entities of the given state without levels"""
         return [self.get_entity_id(e) for e in state]
@@ -124,6 +142,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
                 self.is_valid_entity_with_concentration(r)
                 self.has_non_zero_concentration(r)
                 entity, level = r
+                self.terminate_on_invalid_concentration(entity, level)
                 reactants.append((self.get_entity_id(entity), level))
                 if self.max_concentration < level:
                     self.max_concentration = level
@@ -139,6 +158,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
                 self.is_valid_entity_with_concentration(i)
                 self.has_non_zero_concentration(i)
                 entity, level = i
+                self.terminate_on_invalid_concentration(entity, level)
                 inhibitors.append((self.get_entity_id(entity), level))
                 if self.max_concentration < level:
                     self.max_concentration = level
@@ -154,6 +174,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
                 self.is_valid_entity_with_concentration(p)
                 self.has_non_zero_concentration(p)
                 entity, level = p
+                self.terminate_on_invalid_concentration(entity, level)
                 products.append((self.get_entity_id(entity), level))
 
         return reactants, inhibitors, products

reactics-smt/rsltl_shortcuts.py

@@ -106,3 +106,6 @@ def param_And(*args):
     for arg in args[1:]:
         last = ParamConstraint.f_And(last, arg)
     return last
+
+def param_True():
+    return ParamConstraint.f_TRUE()

rs_testing.py

@@ -26,357 +26,11 @@ def run_tests(cmd_args):
     # heat_shock_response_param(cmd_args)
     # simple_param(cmd_args)
 
-    # gene_expression(cmd_args)
+    # param_gene_expression(cmd_args)
 
-    mutex_bench_main(cmd_args)
-
-def mutex_bench_main(cmd_args):
-
-    if not cmd_args.special_mode:
-        print("Missing special mode parameter")
-        print("*    1 - parametric")
-        print("*    2 - non-parametric (with parametric implementation)")
-        print("*    3 - non-parametric (with non-parametric implementation)")
-        return
-    
-    smode = int(cmd_args.special_mode)
-
-    if smode == 1:
-        mutex_param_bench(cmd_args)
-    elif smode == 2:
-        mutex_nonparam_bench(cmd_args)
-    elif smode == 3:
-        mutex_nonparam_bench_oldimpl(cmd_args)
-    else:
-        print("Unrecognised mode")
-        return
-
-def mutex_param_bench(cmd_args):
+def param_gene_expression(cmd_args):
     """
-    Mutex Benchmark
-    
-    Parametric
-    """
-
-    base_entities = ["out","req","in","act"]
-    shared_entities = ["lock","done","s"]
-    
-    if not cmd_args.scaling_parameter:
-        print("Missing scaling parameter")
-        return
-    n_proc = int(cmd_args.scaling_parameter)
-    
-    r = ReactionSystemWithConcentrationsParam()
-    
-    def E(a,b):
-        return (a + "_" + str(b), 1)
-
-    for i in range(n_proc):
-        for ent in base_entities:
-            r.add_bg_set_entity(E(ent,i))
-
-    for ent in shared_entities:
-        r.add_bg_set_entity((ent, 1))
-    
-    ###################################################
-    
-    Inhib = [("s",1)]
-    
-    for i in range(n_proc):
-        
-        r.add_reaction([E("out",i),E("act",i)],Inhib,[E("req",i)])
-        r.add_reaction([E("out",i)],[E("act",i)],[E("out",i)])
-        
-        for j in range(n_proc):
-            if i != j:
-                r.add_reaction([E("req",i),E("act",i),E("act",j)],Inhib,[E("req",i)])
-        
-        r.add_reaction([E("req",i)],[E("act",i)],[E("req",i)])
-        
-        enter_inhib = [E("act",j) for j in range(n_proc) if i != j] + [("lock",1)]
-        r.add_reaction([E("req",i),E("act",i)],enter_inhib,[E("in",i), ("lock",1)])
-        
-        r.add_reaction([E("in",i),E("act",i)],Inhib,[E("out",i), ("done",1)])
-        r.add_reaction([E("in",i)],[E("act",i)],[E("in",i)])
-    
-    r.add_reaction([("lock",1)],[("done",1)],[("lock",1)])
-    
-    lda1 = r.get_param("lda1")
-    lda2 = r.get_param("lda2")
-    lda3 = r.get_param("lda3")
-    
-    r.add_reaction(lda1,lda2,lda3)
-    
-    ###################################################
-    
-    c = ContextAutomatonWithConcentrations(r)
-    c.add_init_state("0")
-    c.add_state("1")
-    
-    init_ctx = []
-    for i in range(n_proc):
-        init_ctx.append(E("out", i))
-    
-    # the experiments starts with adding x and y:
-    c.add_transition("0", init_ctx, "1")
-    
-    all_act = powerset([E("act",i) for i in range(n_proc)], 2)
-    
-    for actions in all_act:
-        actions = list(actions)
-
-        c.add_transition("1", actions, "1")
-    
-    # for all the remaining steps we have empty context sequences
-    # c.add_transition("1", [], "1")
-    # c.add_transition("1", [("h", 1)], "1")
-    
-    ###################################################
-    
-    rc = ReactionSystemWithAutomaton(r, c)
-    rc.show()
-    
-    f_attack = ltl_F(True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc-1)) == 1))
-    
-    ent_of_Nth_proc = [ent + "_" + str(n_proc-1) for ent in base_entities] + shared_entities
-    disallow = ["in_" + str(n_proc-1)]
-    for ent in r.background_set:
-        if ent not in ent_of_Nth_proc:
-            disallow.append(ent)
-    
-    # disallow = ["in_0", "in_" + str(n_proc)] #, "req_0", "req_1"]
-    lda1_disallow = [param_entity(lda1, ent) == 0 for ent in disallow]
-    lda2_disallow = [param_entity(lda2, ent) == 0 for ent in disallow]
-    lda3_disallow = [param_entity(lda3, ent) == 0 for ent in disallow]
-    lda_disallow = lda1_disallow + lda2_disallow + lda3_disallow
-    
-    # for bent in base_entities:
-    #     print(param_entity(lda3, bent + "_0"))
-    
-    param_constr = param_And(*lda_disallow)
-    
-    smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
-    smt_rsc.check_rsltl(formulae_list=[f_attack], param_constr=param_constr) #, max_level=4, cont_if_sat=True)
-
-    log_suffix = ""
-    if cmd_args.optimise:
-        log_suffix = "_OPT"
-
-    time=0
-    mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)
-    filename_t="bench_mutex_param" + log_suffix + "_time.dat"
-    filename_m="bench_mutex_param" + log_suffix + "_mem.dat"
-    time=smt_rsc.get_verification_time()
-
-    with open(filename_t, 'a') as f:
-        log_str="{:d} {:f}\n".format(n_proc, time)
-        f.write(log_str)
-    
-    with open(filename_m, 'a') as f:
-        log_str="{:d} {:f}\n".format(n_proc, mem_usage)
-        f.write(log_str)
-
-def mutex_nonparam_bench(cmd_args):
-    """
-    Mutex Benchmark
-    
-    Parametric
-    """
-
-    base_entities = ["out","req","in","act"]
-    shared_entities = ["lock","done","s"]
-    
-    if not cmd_args.scaling_parameter:
-        raise RuntimeError("Missing scaling parameter")
-    n_proc = int(cmd_args.scaling_parameter)
-    
-    r = ReactionSystemWithConcentrationsParam()
-    
-    def E(a,b):
-        return (a + "_" + str(b), 1)
-
-    for i in range(n_proc):
-        for ent in base_entities:
-            r.add_bg_set_entity(E(ent,i))
-
-    for ent in shared_entities:
-        r.add_bg_set_entity((ent, 1))
-    
-    ###################################################
-    
-    Inhib = [("s",1)]
-    
-    for i in range(n_proc):
-        
-        r.add_reaction([E("out",i),E("act",i)],Inhib,[E("req",i)])
-        r.add_reaction([E("out",i)],[E("act",i)],[E("out",i)])
-        
-        for j in range(n_proc):
-            if i != j:
-                r.add_reaction([E("req",i),E("act",i),E("act",j)],Inhib,[E("req",i)])
-        
-        r.add_reaction([E("req",i)],[E("act",i)],[E("req",i)])
-        
-        enter_inhib = [E("act",j) for j in range(n_proc) if i != j] + [("lock",1)]
-        r.add_reaction([E("req",i),E("act",i)],enter_inhib,[E("in",i), ("lock",1)])
-        
-        r.add_reaction([E("in",i),E("act",i)],Inhib,[E("out",i), ("done",1)])
-        r.add_reaction([E("in",i)],[E("act",i)],[E("in",i)])
-    
-    r.add_reaction([("lock",1)],[("done",1)],[("lock",1)])
-    
-    r.add_reaction([E("out",n_proc-1)],[("s",1)],[("done",1),E("req",n_proc-1)])
-    
-    ###################################################
-    
-    c = ContextAutomatonWithConcentrations(r)
-    c.add_init_state("0")
-    c.add_state("1")
-    
-    init_ctx = []
-    for i in range(n_proc):
-        init_ctx.append(E("out", i))
-    
-    # the experiments starts with adding x and y:
-    c.add_transition("0", init_ctx, "1")
-    
-    all_act = powerset([E("act",i) for i in range(n_proc)], 2)
-    
-    for actions in all_act:
-        actions = list(actions)
-
-        c.add_transition("1", actions, "1")
-    
-    # for all the remaining steps we have empty context sequences
-    # c.add_transition("1", [], "1")
-    # c.add_transition("1", [("h", 1)], "1")
-    
-    ###################################################
-    
-    rc = ReactionSystemWithAutomaton(r, c)
-    rc.show()
-    
-    f_attack = ltl_F(True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc-1)) == 1))
-    
-    smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
-    smt_rsc.check_rsltl(formulae_list=[f_attack])
-
-    time=0
-    mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)
-    filename_t="bench_mutex_nonparam_time.dat"
-    filename_m="bench_mutex_nonparam_mem.dat"
-    time=smt_rsc.get_verification_time()
-
-    with open(filename_t, 'a') as f:
-        log_str="{:d} {:f}\n".format(n_proc, time)
-        f.write(log_str)
-    
-    with open(filename_m, 'a') as f:
-        log_str="{:d} {:f}\n".format(n_proc, mem_usage)
-        f.write(log_str)
-
-def mutex_nonparam_bench_oldimpl(cmd_args):
-    """
-    Mutex Benchmark
-    
-    Parametric
-    """
-
-    base_entities = ["out","req","in","act"]
-    shared_entities = ["lock","done","s"]
-    
-    if not cmd_args.scaling_parameter:
-        raise RuntimeError("Missing scaling parameter")
-    n_proc = int(cmd_args.scaling_parameter)
-    
-    r = ReactionSystemWithConcentrations()
-    
-    def E(a,b):
-        return (a + "_" + str(b), 1)
-
-    for i in range(n_proc):
-        for ent in base_entities:
-            r.add_bg_set_entity(E(ent,i))
-
-    for ent in shared_entities:
-        r.add_bg_set_entity((ent, 1))
-    
-    ###################################################
-    
-    Inhib = [("s",1)]
-    
-    for i in range(n_proc):
-        
-        r.add_reaction([E("out",i),E("act",i)],Inhib,[E("req",i)])
-        r.add_reaction([E("out",i)],[E("act",i)],[E("out",i)])
-        
-        for j in range(n_proc):
-            if i != j:
-                r.add_reaction([E("req",i),E("act",i),E("act",j)],Inhib,[E("req",i)])
-        
-        r.add_reaction([E("req",i)],[E("act",i)],[E("req",i)])
-        
-        enter_inhib = [E("act",j) for j in range(n_proc) if i != j] + [("lock",1)]
-        r.add_reaction([E("req",i),E("act",i)],enter_inhib,[E("in",i), ("lock",1)])
-        
-        r.add_reaction([E("in",i),E("act",i)],Inhib,[E("out",i), ("done",1)])
-        r.add_reaction([E("in",i)],[E("act",i)],[E("in",i)])
-    
-    r.add_reaction([("lock",1)],[("done",1)],[("lock",1)])
-    
-    r.add_reaction([E("out",n_proc-1)],[("s",1)],[("done",1),E("req",n_proc-1)])
-    
-    ###################################################
-    
-    c = ContextAutomatonWithConcentrations(r)
-    c.add_init_state("0")
-    c.add_state("1")
-    
-    init_ctx = []
-    for i in range(n_proc):
-        init_ctx.append(E("out", i))
-    
-    # the experiments starts with adding x and y:
-    c.add_transition("0", init_ctx, "1")
-    
-    all_act = powerset([E("act",i) for i in range(n_proc)], 2)
-    
-    for actions in all_act:
-        actions = list(actions)
-
-        c.add_transition("1", actions, "1")
-    
-    # for all the remaining steps we have empty context sequences
-    # c.add_transition("1", [], "1")
-    # c.add_transition("1", [("h", 1)], "1")
-    
-    ###################################################
-    
-    rc = ReactionSystemWithAutomaton(r, c)
-    rc.show()
-    
-    f_attack = ltl_F(True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc-1)) == 1))
-    
-    smt_rsc = SmtCheckerRSC(rc)
-    smt_rsc.check_rsltl(formula=f_attack)
-
-    time=0
-    mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)
-    filename_t="bench_mutex_nonparam_oldimpl_time.dat"
-    filename_m="bench_mutex_nonparam_oldimpl_mem.dat"
-    time=smt_rsc.get_verification_time()
-
-    with open(filename_t, 'a') as f:
-        log_str="{:d} {:f}\n".format(n_proc, time)
-        f.write(log_str)
-    
-    with open(filename_m, 'a') as f:
-        log_str="{:d} {:f}\n".format(n_proc, mem_usage)
-        f.write(log_str)
-
-def gene_expression(cmd_args):
-    """
-    Simple gene expression example
+    Simple gene expression example with parameters
     """
     r = ReactionSystemWithConcentrationsParam()
 
@@ -391,8 +45,14 @@ def gene_expression(cmd_args):
 
     all_entities = set(r.background_set)
 
+    lda0 = r.get_param("lda0")
+    lda1 = r.get_param("lda1")
+    lda2 = r.get_param("lda2")
+    lda3 = r.get_param("lda3")
+
     r.add_reaction([("x",1)],[("h",1)],[("x",1)])
-    r.add_reaction([("x",1)],[("h",1)],[("xp",1)])
+    # r.add_reaction([("x",1)],[("h",1)],[("xp",1)])
+    r.add_reaction(lda0, [("h",1)],[("xp",1)])
     r.add_reaction([("x",1),("xp",1)],[("h",1)],[("X",1)])
 
     r.add_reaction([("X",1),("Y",1)],[("h",1)],[("Q",1)])
@@ -401,9 +61,6 @@ def gene_expression(cmd_args):
     # r.add_reaction([("y",1)],[("h",1)],[("y",1)])
     # r.add_reaction([("y",1)],[("Q",1)],[("yp",1)])
     # r.add_reaction([("y",1),("yp",1)],[("h",1)],[("Y",1)])
-    lda1 = r.get_param("lda1")
-    lda2 = r.get_param("lda2")
-    lda3 = r.get_param("lda3")
 
     r.add_reaction([("y",1)],[("h",1)],lda1)
     r.add_reaction(lda2,[("h",1)],[("yp",1)])
@@ -454,6 +111,12 @@ def gene_expression(cmd_args):
 
     obs_1 = ltl_And(phi_r, phi_c1, phi_c2, delayed_Q)
     
+    # Observation related to A_x:
+    obs_2 = ltl_G(bag_entity("h") == 0, ltl_Implies(
+            bag_entity("x") > 0,
+            ltl_X(True, bag_And(bag_entity("x") > 0, bag_entity("xp") > 0))))
+    
+    
     # obs_2 = ltl_And(f_y2, reach_y, reach_Y, delayed_Y, delayed_Q)
 
     # f_x2 = ltl_G(True, ltl_Implies(
@@ -461,13 +124,33 @@ def gene_expression(cmd_args):
     #     ltl_X(bag_Not("h"), exact_state("X", all_entities))))
     #
     
-    param_constr = param_And(param_entity(lda3, "Y") > 0, param_entity(lda2, "Q") == 0, param_entity(lda1, "yp") == 0, param_entity(lda1, "Y") == 0)
+    related_to_x = ["x", "xp", "X"]
+    related_to_y = ["y", "yp", "Y"]
+    params_for_x = [lda0]
+    params_for_y = [lda1, lda2, lda3]
+    
+    
+    
+    no_x_in_y = param_True()
+    for par in params_for_y:
+        for ent in related_to_x:
+            no_x_in_y = param_And(no_x_in_y, param_entity(par, ent) == 0)
+    
+    no_y_in_x = param_True()
+    for par in params_for_x:
+        for ent in related_to_y:
+            no_y_in_x = param_And(no_y_in_x, param_entity(par, ent) == 0)
+    
+    # param_constr = param_And(param_entity(lda3, "Y") > 0, param_entity(lda3, "X") == 0, param_entity(lda2, "Q") == 0, param_entity(lda1, "yp") == 0, param_entity(lda1, "Y") == 0)
+    param_constr = param_And(no_y_in_x, no_x_in_y)
         
     smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
     #
-    smt_rsc.check_rsltl(formulae_list=[obs_1], param_constr=param_constr) #, max_level=4, cont_if_sat=True)
+    smt_rsc.check_rsltl(
+        formulae_list=[obs_1,obs_2],
+        param_constr=param_constr,
+    ) #, max_level=4, cont_if_sat=True)
 
-    # smt_rsc.check_rsltl(formula=f_x1, print_witness=True)
 
 def gene_expression_full(cmd_args):
     """
@@ -962,236 +645,3 @@ def heat_shock_response(print_system=True):
 def state_translate_rsc2rs(p):
     return [e[0] + "#" + str(e[1]) for e in p]    
 
-
-def scalable_chain(print_system=False):
-    
-    if len(sys.argv) < 1+3:
-        print("arguments: <chainLen> <maxConc> <formulaNumber>")
-        exit(1)
-
-    chainLen=int(sys.argv[1]) # chain length
-    maxConc=int(sys.argv[2]) # depth (max concentration)
-    formula_number=int(sys.argv[3])
-        
-    if chainLen < 1 or maxConc < 1:
-        print("be reasonable")
-        exit(1)
-    if not formula_number in range(1,5+1):
-        print("formulaNumber must be in 1..5")
-        exit(1)
-    
-    r = ReactionSystemWithConcentrations()
-    r.add_bg_set_entity(("inc",1))
-    r.add_bg_set_entity(("dec",1))
-    
-    for i in range(1,chainLen+1):
-        r.add_bg_set_entity(("e_" + str(i),maxConc))
-    
-    for i in range(1,chainLen+1):
-        ent = "e_" + str(i)
-        r.add_reaction_inc(ent, "inc", [(ent, 1)],[(ent,maxConc)])
-        r.add_reaction_dec(ent, "dec", [(ent, 1)],[])
-        if i < chainLen:
-            r.add_reaction([(ent,maxConc)],[],[("e_"+str(i+1),1)])
-
-    r.add_reaction([("e_" + str(chainLen),maxConc)],[("dec",1)],[("e_" + str(chainLen),maxConc)])
-        
-    c = ContextAutomatonWithConcentrations(r)
-    c.add_init_state("init")
-    c.add_state("working")
-    c.add_transition("init", [("e_1",1),("inc",1)], "working")
-    c.add_transition("working", [("inc",1)], "working")
-    
-    rc = ReactionSystemWithAutomaton(r,c)
-    
-    if print_system:
-        rc.show()
-    
-    smt_rsc = SmtCheckerRSC(rc)
-
-    if formula_number == 1:
-        f_1 = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) >= maxConc) )
-        smt_rsc.check_rsltl(formula=f_1)
-    elif formula_number == 2:
-        f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) )
-        for i in range(chainLen-1,0,-1):
-            f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, f_tmp & (BagDescription.f_entity('e_'+str(i)) == maxConc) )
-        f_2 = f_tmp
-        smt_rsc.check_rsltl(formula=f_2)
-    elif formula_number == 3:
-        f_3 = Formula_rsLTL.f_G( BagDescription.f_TRUE(),
-            Formula_rsLTL.f_Implies(
-                (BagDescription.f_entity('e_1') == 1),
-                Formula_rsLTL.f_F(
-                    BagDescription.f_entity("inc") > 0,
-                    (BagDescription.f_entity('e_'+str(chainLen)) == maxConc)
-                )
-            )
-        )
-        print(i)
-        smt_rsc.check_rsltl(formula=f_3)
-    elif formula_number == 4:
-        f_4 = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') == maxConc )
-        smt_rsc.check_rsltl(formula=f_4)
-        
-    elif formula_number == 5:
-        f_5 = Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_U( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') > 0, BagDescription.f_entity('e_2') > 0 ) )
-        smt_rsc.check_rsltl(formula=f_5)
-    
-    ###########################################################################
-
-    time=0
-    mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)
-    filename_t="bench_rsc_F" + str(formula_number) + "_time.log"
-    filename_m="bench_rsc_F" + str(formula_number) + "_mem.log"
-    time=smt_rsc.get_verification_time()
-
-    f=open(filename_t, 'a')    
-    log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n"
-    f.write(log_str)
-    f.close()
-    
-    f=open(filename_m, 'a')
-    log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n"
-    f.write(log_str)
-    f.close()
-
-
-def test_rsLTL():
-
-    r = ReactionSystemWithConcentrations()
-    r.add_bg_set_entity(("inc",2))
-    r.add_bg_set_entity(("ent1",1))
-    r.add_bg_set_entity(("ent2",5))
-    r.add_reaction([("ent2",1),("inc",1)],[],[("ent2",2)])
-    r.add_reaction([("ent2",2)],[],[("ent2",2)])
-
-    c = ContextAutomatonWithConcentrations(r)
-    c.add_init_state("init")
-    c.add_state("working")
-    c.add_transition("init", [("ent2",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) ) ) )
-    x = Formula_rsLTL.f_G((BagDescription.f_entity("inc") > 0), (BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3))
-    
-    #x = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("ent2") == 2) )
-    
-    print(x)
-    
-    rc = ReactionSystemWithAutomaton(r,c)
-    rc.show()
-    
-    checker = SmtCheckerRSC(rc)
-    checker.check_rsltl(formula=x)
-    
-    # checker.dummy_unroll(10)
-    # e = rsLTL_Encoder(checker)
-    # print(checker.get_loop_encodings())
-    # print(e.encode(x, 0, 10))
-
-def test_extended_automaton():
-    
-    r = ReactionSystem()
-    r.add_bg_set_entity("a")
-    r.add_bg_set_entity("b")
-    r.add_bg_set_entity("inc")
-    r.add_bg_set_entity("dec")
-    r.add_bg_set_entity("decx")
-    r.add_bg_set_entity("baam")
-
-    c1 = ExtendedContextAutomaton(r)
-    c1.add_init_state("init")
-    c1.name = "catest"
-    c1.add_state("working")
-    c1.add_action("act1")
-    c1.add_action("act2")
-    c1.add_transition("init", ["act1", "act2"], (["a"],["b"],["inc","dec"]), "working")
-    c1.add_transition("working", ["act2"], ([],[],["inc"]), "working")
-
-    c2 = ExtendedContextAutomaton(r)
-    c2.add_init_state("init")
-    c2.name = "c2"
-    c2.add_state("working")
-    c2.add_action("act1")
-    c2.add_action("act2")
-    c2.add_transition("init", ["act1", "act2"], ([],[],["inc"]), "working")
-    c2.add_transition("working", ["act2"], ([],[],["inc"]), "working")
-    
-    c3 = ExtendedContextAutomaton(r)
-    c3.add_init_state("init")
-    c3.name = "c3"
-    c3.add_state("working")
-    c3.add_action("act1")
-    c3.add_transition("init", ["act1"], ([],[],["inc"]), "working")
-    
-    c4 = ExtendedContextAutomaton(r)
-    c4.add_init_state("init")
-    c4.name = "c4"
-    c4.add_state("w")
-    c4.add_action("action_x")
-    c4.add_transition("init", ["action_x"], ([],[],["baam"]), "w")
-    #
-    # c4 = ExtendedContextAutomaton(r)
-    # c4.add_init_state("init")
-    # c4.name = "c4"
-    # c4.add_state("working")
-    # c4.add_action("act1")
-    # c4.add_action("act42")
-    # c4.add_transition("init", ["act1", "act42"], ([],[],["inc"]), "working")
-    # c4.add_transition("working", ["act42"], ([],[],["inc"]), "working")
-    #
-    # c5 = ExtendedContextAutomaton(r)
-    # c5.add_init_state("init")
-    # c5.name = "c5"
-    # c5.add_state("working")
-    # c5.add_action("act1")
-    # c5.add_action("act2")
-    # c5.add_transition("init", ["act1", "act2"], ([],[],["inc"]), "working")
-    # c5.add_transition("working", ["act2"], ([],[],["inc"]), "working")
-
-    na = NetworkOfContextAutomata(r, [c1,c2,c3,c4])
-
-    rna = ReactionSystemWithNetworkOfAutomata(r,na)
-
-    rna.show()
-    
-    checker = SmtCheckerRSNA(rna)
-    
-    checker.check_reachability([])
-
-def process():
-    
-    # rs_examples.run_counter_exp()
-    rs_examples.chain_reaction(print_system=True)
-    # rs_examples.heat_shock_response()
-    
-    
-
-# RS:
-# rsca = rs_examples.ca_toy_ex1()
-# rsca.show()
-# 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 = SmtCheckerRS(rsca)
-# smt.check_reachability(rs_examples.ca_bitctr_property(N), print_time=True)
-
-# Distributed RS:
-#drs = rs_examples.drs_mutex(N)
-#drs.show()
-
-#smt = SmtCheckerDistribRS(drs,debug_level=0)
-#smt.check_reachability(rs_examples.drs_mutex_property1(N),
-#    exclusive_state=False,
-#    max_level=10,
-#    print_time=True,
-#    print_mem=True)
-
-# drs = rs_examples.drs_toy_ex1()
-# drs.show()
-#
-# smt = SmtCheckerDistribRS(drs,debug_level=3)
-# smt.check_reachability(rs_examples.drs_toy_ex1_property1(),max_level=10,print_time=True)