diff --git a/rs/extended_context_automaton.py b/rs/extended_context_automaton.py index 870226d..6f7449e 100644 --- a/rs/extended_context_automaton.py +++ b/rs/extended_context_automaton.py @@ -50,6 +50,14 @@ class ExtendedContextAutomaton(ContextAutomaton): else: return set() + def can_produce_entity(self, entity): + """Check if the automaton can produce an entity""" + + if entity in self._actions_for_products: + return True + else: + return False + def add_transition(self, src, actions, ctx_reaction, dst): """Adds a transition diff --git a/rs/network_of_context_automata.py b/rs/network_of_context_automata.py index 86b1931..d9b2a63 100644 --- a/rs/network_of_context_automata.py +++ b/rs/network_of_context_automata.py @@ -33,6 +33,10 @@ class NetworkOfContextAutomata(object): """Returns the set of entities that can potentially be produced by the automata in the network""" return self._prod_entities + @property + def automata_ids(self): + return set(range(len(self.automata))) + def sanity_check(self): """Performs a sanity check of the network of automata""" diff --git a/rs_testing.py b/rs_testing.py index 14d21c1..844a0e8 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -10,10 +10,12 @@ def run_tests(): 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") @@ -21,7 +23,7 @@ def test_extended_automaton(): c1.add_state("working") c1.add_action("act1") c1.add_action("act2") - c1.add_transition("init", ["act1", "act2"], ([],[],["inc","dec"]), "working") + c1.add_transition("init", ["act1", "act2"], (["a"],["b"],["inc","dec"]), "working") c1.add_transition("working", ["act2"], ([],[],["inc"]), "working") c2 = ExtendedContextAutomaton(r) @@ -39,6 +41,13 @@ def test_extended_automaton(): 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") @@ -58,7 +67,7 @@ def test_extended_automaton(): # c5.add_transition("init", ["act1", "act2"], ([],[],["inc"]), "working") # c5.add_transition("working", ["act2"], ([],[],["inc"]), "working") - na = NetworkOfContextAutomata(r, [c1,c2,c3]) + na = NetworkOfContextAutomata(r, [c1,c2,c3,c4]) rna = ReactionSystemWithNetworkOfAutomata(r,na) diff --git a/smt/smt_checker_rs_na.py b/smt/smt_checker_rs_na.py index 3905eb5..428a46f 100644 --- a/smt/smt_checker_rs_na.py +++ b/smt/smt_checker_rs_na.py @@ -38,7 +38,7 @@ class SmtCheckerRSNA(SmtCheckerRS): for ca_id in range(self.number_of_automata): ca_states.append(Int("CA"+str(level)+"_a"+str(ca_id)+"_state")) self.v_canet_states.append(ca_states) - + # We do not encode actions when there are no transitions needed. if level > 0: ca_actions = [] @@ -56,10 +56,86 @@ class SmtCheckerRSNA(SmtCheckerRS): canet_init_state_enc = simplify(And(canet_init_state_enc, ca_init_state_enc)) return canet_init_state_enc - + def enc_transition_relation(self, level): return simplify(And(self.enc_rs_trans(level), self.enc_automaton_trans(level))) + def enc_reactants_ids(self, level, set_of_ids): + """Encodes reactants given by their ids in RS""" + + enc_ents = True + for r_id in set_of_ids: + enc_ents = simplify(And(enc_ents, self.v[level][r_id])) + return enc_ents + + def enc_inhibitors_ids(self, level, set_of_ids): + """Encodes inhibitors given by their ids in RS""" + + enc_ents = True + for i_id in set_of_ids: + enc_ents = simplify(And(enc_ents, Not(self.v[level][i_id]))) + return enc_ents + + def enc_context_single_transition(self, level, automaton, transition): + """""" + + src_id, act_ids, (r_ids, i_ids, p_ids), dst_id = transition + + enc_transition = self.v_canet_states[level][automaton] == src_id + enc_transition = simplify(And(enc_transition, self.enc_reactants_ids(level, r_ids), self.enc_inhibitors_ids(level, i_ids))) + enc_transition = simplify(And(enc_transition, self.v_canet_states[level+1][automaton] == dst_id)) + # ACTIONS NOT ENCODED! + + print(enc_transition) + return enc_transition + + def enc_context_entity_production(self, level, entity): + """Encodes the automata transitions and the production for a given entity""" + + enc_production = False + + actions_producing_ent = self.canet.get_actions_producing_entity(entity) + enc_prod_action = False + + for act in actions_producing_ent: + + # automata_with_act = self.canet.get_automata_with_action(act) + enc_aut_with_act = True + + for aut_id in self.canet.automata_ids: + + aut = self.canet.automata[aut_id] + + t_producing_entity = aut.get_transitions_producing_entity(entity) + + enc_t_producing_entity = False + + if t_producing_entity: + # for the automata that produce the entity we take + # all the transitions that produce it: + + + for t in t_producing_entity: + enc_t_producing_entity = simplify(Or(enc_t_producing_entity, self.enc_context_single_transition(level, aut_id, t))) + + else: + # for all the automata that do not produce the entity + # we encode the transitions that synchronise with the action: + + pass + + enc_aut_with_act = simplify(And(enc_aut_with_act, enc_t_producing_entity)) + + enc_prod_action = simplify(Or(enc_prod_action, enc_aut_with_act)) + + # TODO + # for aut in remaining_automata_which_do_not_contain_act: + # encode no change + + enc_production = enc_prod_action + + return enc_production + def enc_automaton_trans(self, level): """Encodes the transition relation for the context automaton""" @@ -68,19 +144,23 @@ class SmtCheckerRSNA(SmtCheckerRS): prod_context = self.canet.prod_entities never_produced_context = self.rs.set_of_bgset_ids - prod_context - # producible entities: + # (1) producible entities: for ent in prod_context: - actions_producing_ent = self.canet.get_actions_producing_entity(ent) - for act in actions_producing_ent: - automata_with_act = self.canet.get_automata_with_action(act) - for aut_id in automata_with_act: - aut = self.canet.automata[aut_id] + enc_trans = simplify(And(enc_trans, self.enc_context_entity_production(level, ent))) - # entities that are never produced: + + # (2) entities that are never produced: + + # (3) TODO: no entity, empty set of entities: transitions with no entities + # simplify((enc_trans, self.enc_context_no_entity_production(level))) + # TRANSITIONS PRODUCING EMPTY SETS + + print(enc_trans) return enc_trans def check_reachability(self, state, print_witness=True, print_time=True, print_mem=True): + """The main method for checking reachability""" self.prepare_all_variables() self.solver.add(self.enc_init_state(0))