diff --git a/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml b/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml index ed13a4fb27..15ae09b96b 100644 --- a/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml +++ b/KaSa_rep/reachability_analysis/site_across_bonds_domain.ml @@ -4,7 +4,7 @@ * Jérôme Feret & Ly Kim Quyen, project Antique, INRIA Paris * * Creation: 2016, the 31th of March - * Last modification: Time-stamp: + * Last modification: Time-stamp: * * Abstract domain to record relations between pair of sites in connected agents. * @@ -972,8 +972,31 @@ struct (*APPLY RULE*) (***************************************************************************) + let check_association_list + parameters error bdu_false + pair + check + dynamic + = + let store_result = get_value dynamic in + let handler = get_mvbdu_handler dynamic in + let error, handler, mvbdu = + Ckappa_sig.Views_bdu.mvbdu_of_association_list + parameters handler error check + in + let error, handler, bool = + Site_across_bonds_domain_type.check + parameters error bdu_false handler + pair + mvbdu + store_result + in + let dynamic = set_mvbdu_handler handler dynamic in + error, dynamic, bool (*there is an action binding in the domain of a rule*) + + let build_mvbdu_association_list parameters error bdu_false kappa_handler dump_title bool modified_sites pair pair_list dynamic = let store_result = get_value dynamic in @@ -1205,19 +1228,53 @@ struct let dynamic = set_global_dynamic_information global_dynamic dynamic in error, dynamic, precondition, state_list + + let get_state_of_site_in_precondition_2 - error static dynamic rule agent_id - (site_type_x, agent_type_y, site_type_y) - site_type'_y + error static dynamic rule + agent_id agent_type site precondition = - let defined_in = Communication.LHS rule in - get_state_of_site_in_pre_post_condition_2 - error static dynamic - agent_id - (site_type_x, agent_type_y, site_type_y) - site_type'_y - defined_in - precondition + + let path = + { + Communication.defined_in = Communication.LHS rule; + path = + { + Communication.agent_id = agent_id; + Communication.relative_address = []; + Communication.site = site} + } + in + let error, global_dynamic, precondition, state_list_lattice = + Communication.get_state_of_site + error + precondition + (get_global_static_information static) + (get_global_dynamic_information dynamic) + path + in + let error, state_list = + match state_list_lattice with + | Usual_domains.Val l -> error, l + | Usual_domains.Undefined -> error, [] + | Usual_domains.Any -> + let parameter = get_parameter static in + let error, () = + if Remanent_parameters.get_view_analysis parameter + then + Exception.warn + (get_parameter static) error __POS__ Exit () + else + error, () + in + let kappa_handler = get_kappa_handler static in + Handler.state_list + parameter kappa_handler error agent_type site + in + let dynamic = set_global_dynamic_information global_dynamic dynamic in + error, dynamic, precondition, state_list + + let get_state_of_site_in_postcondition_2 error static dynamic rule agent_id @@ -1232,6 +1289,7 @@ struct defined_in precondition + type pos = Fst | Snd let get_partition_modified pos static = @@ -1260,6 +1318,8 @@ struct (site_type_y, agent_type_x, site_type_x) site_type'_x precondition + + let get_potential_tuple_pair parameters error (agent, site) empty_map map = let error, result = match @@ -1341,13 +1401,47 @@ struct | Snd -> site_type'_x)) __POS__ Exit in + let error', dynamic, precondition, state_list_other = + let error, agent = + match + Ckappa_sig.Agent_id_quick_nearly_Inf_Int_storage_Imperatif.get + parameters + error + agent_id_mod + rule.Cckappa_sig.e_rule_c_rule.Cckappa_sig.rule_lhs.Cckappa_sig.views + with + | error, None -> + Exception.warn parameters error __POS__ Exit Cckappa_sig.Ghost + | error, Some a -> error, a + in + match agent with + | Cckappa_sig.Ghost + | Cckappa_sig.Unknown_agent _ + | Cckappa_sig.Dead_agent _ -> + error, dynamic, precondition, [] + | Cckappa_sig.Agent agent -> + get_state_of_site_in_precondition_2 + error static dynamic + (rule_id, rule) + agent_id_mod agent_type_mod site_type_mod + precondition + in + let error = + Exception.check_point + Exception.warn + parameters error error' + ~message:(context rule_id agent_id_mod site_type_mod) + __POS__ Exit + in (*-----------------------------------------------------------*) let error, bool, dynamic, precondition, modified_sites = - match state'_list_other with - | [] | _::_::_ -> - (* we know for sure that the site has not been modified *) - error, bool, dynamic, precondition, modified_sites - | [_] -> + let not_modified = + match state'_list_other with + | [] | _::_::_ -> true +(* we know for sure that the site has not been modified *) + + | [_] -> false + in List.fold_left (fun (error, bool, dynamic, precondition, modified_sites) state'_other -> @@ -1364,17 +1458,58 @@ struct (agent_type_x, site_type_x, site_type'_x,state_x), (agent_type_y, site_type_y, site_type'_y,state_y) in - let error, bool, dynamic, modified_sites = - build_mvbdu_association_list + let check = + match state_list_other,pos + with + ([] | _::_::_),_ -> [] + | [a],Fst -> + [Ckappa_sig.fst_site, a] + | [a],Snd -> + [Ckappa_sig.snd_site, a] + in + let check = + if not_modified + then + match pos with + | Fst -> + (* to do: add info about the other site *) + (* if the bond between site_type_x and site_type_y + has not been created by the rule *) + (* this is the state before the modification *) + (* otherwise, nothing to check *) + (Ckappa_sig.snd_site, state'_other)::check + | Snd -> + (* to do: add info about the other site *) + (* if the bond between site_type_x and site_type_y + has not been created by the rule *) + (* this is the state before the modification *) + (* this is the state before the modification *) + (Ckappa_sig.fst_site, state'_other)::check + else + check + in + let error, dynamic, unmodified_sites_ok = + check_association_list parameters error bdu_false - kappa_handler dump_title - bool - modified_sites pair - pair_list + check dynamic in - error, bool, dynamic, precondition, modified_sites + if unmodified_sites_ok + then + let error, bool, dynamic, modified_sites = + build_mvbdu_association_list + parameters error bdu_false + kappa_handler dump_title + bool + modified_sites + pair + pair_list + dynamic + in + error, bool, dynamic, precondition, modified_sites + else + error, bool, dynamic, precondition, modified_sites ) (error, bool, dynamic, precondition, modified_sites) state'_list_other diff --git a/KaSa_rep/reachability_analysis/site_across_bonds_domain_type.ml b/KaSa_rep/reachability_analysis/site_across_bonds_domain_type.ml index 5a46a9e9a0..2f6f3860c9 100644 --- a/KaSa_rep/reachability_analysis/site_across_bonds_domain_type.ml +++ b/KaSa_rep/reachability_analysis/site_across_bonds_domain_type.ml @@ -4,7 +4,7 @@ * Jérôme Feret & Ly Kim Quyen, project Antique, INRIA Paris-Rocquencourt * * Creation: 2016, the 31th of March - * Last modification: Time-stamp: + * Last modification: Time-stamp: * * Abstract domain to record relations between pair of sites in connected agents. * @@ -504,6 +504,25 @@ let add_sites_from_tuples parameters error tuple modified_sites = (error, modified_sites) [agent,site1;agent,site2;agent',site1';agent',site2'] +let check + parameters error bdu_false handler + pair + mvbdu + store_result + = + let error, bdu_old = + get_mvbdu_from_tuple_pair parameters error pair bdu_false store_result + in + let error, handler, new_bdu = + Ckappa_sig.Views_bdu.mvbdu_and + parameters handler error bdu_old mvbdu + in + if Ckappa_sig.Views_bdu.equal new_bdu bdu_false + then + error, handler, false + else + error, handler, true + let add_link_and_check parameter error bdu_false handler kappa_handler bool dump_title x mvbdu modified_sites store_result = let error, bdu_old = diff --git a/models/test_suite/CMSB_paper/dimer/output/LOG.ref b/models/test_suite/CMSB_paper/dimer/output/LOG.ref index 4dac95c8fa..e0ed19a273 100644 --- a/models/test_suite/CMSB_paper/dimer/output/LOG.ref +++ b/models/test_suite/CMSB_paper/dimer/output/LOG.ref @@ -42,11 +42,6 @@ R(c!1),R(c!1) => v R(c!1,cr),R(c!1,cr) v R(c!1,cr),R(c!1,cr!R.n) ] -R(c!1),R(c!1) => - [ - R(c!1,cr!R.n),R(c!1,n!R.cr) - v R(c!1,cr),R(c!1,n) - ] R(c!1),R(c!1) => [ R(c!1,n!R.cr),R(c!1,n) diff --git a/models/test_suite/CMSB_paper/dimer_all_domains/output/LOG.ref b/models/test_suite/CMSB_paper/dimer_all_domains/output/LOG.ref index 4dac95c8fa..e0ed19a273 100644 --- a/models/test_suite/CMSB_paper/dimer_all_domains/output/LOG.ref +++ b/models/test_suite/CMSB_paper/dimer_all_domains/output/LOG.ref @@ -42,11 +42,6 @@ R(c!1),R(c!1) => v R(c!1,cr),R(c!1,cr) v R(c!1,cr),R(c!1,cr!R.n) ] -R(c!1),R(c!1) => - [ - R(c!1,cr!R.n),R(c!1,n!R.cr) - v R(c!1,cr),R(c!1,n) - ] R(c!1),R(c!1) => [ R(c!1,n!R.cr),R(c!1,n) diff --git a/models/test_suite/CMSB_paper/dimer_cm_views_site_across_bonds/output/LOG.ref b/models/test_suite/CMSB_paper/dimer_cm_views_site_across_bonds/output/LOG.ref index f3a3447e93..b4934a2a39 100644 --- a/models/test_suite/CMSB_paper/dimer_cm_views_site_across_bonds/output/LOG.ref +++ b/models/test_suite/CMSB_paper/dimer_cm_views_site_across_bonds/output/LOG.ref @@ -42,11 +42,6 @@ R(c!1),R(c!1) => v R(c!1,cr),R(c!1,cr) v R(c!1,cr),R(c!1,cr!R.n) ] -R(c!1),R(c!1) => - [ - R(c!1,cr!R.n),R(c!1,n!R.cr) - v R(c!1,cr),R(c!1,n) - ] R(c!1),R(c!1) => [ R(c!1,n!R.cr),R(c!1,n) diff --git a/models/test_suite/CMSB_paper/dimer_views_site_across_bonds/output/LOG.ref b/models/test_suite/CMSB_paper/dimer_views_site_across_bonds/output/LOG.ref index f3a3447e93..b4934a2a39 100644 --- a/models/test_suite/CMSB_paper/dimer_views_site_across_bonds/output/LOG.ref +++ b/models/test_suite/CMSB_paper/dimer_views_site_across_bonds/output/LOG.ref @@ -42,11 +42,6 @@ R(c!1),R(c!1) => v R(c!1,cr),R(c!1,cr) v R(c!1,cr),R(c!1,cr!R.n) ] -R(c!1),R(c!1) => - [ - R(c!1,cr!R.n),R(c!1,n!R.cr) - v R(c!1,cr),R(c!1,n) - ] R(c!1),R(c!1) => [ R(c!1,n!R.cr),R(c!1,n) diff --git a/models/test_suite/CMSB_paper/dimer_views_site_across_bonds_double_bonds/output/LOG.ref b/models/test_suite/CMSB_paper/dimer_views_site_across_bonds_double_bonds/output/LOG.ref index 4dac95c8fa..e0ed19a273 100644 --- a/models/test_suite/CMSB_paper/dimer_views_site_across_bonds_double_bonds/output/LOG.ref +++ b/models/test_suite/CMSB_paper/dimer_views_site_across_bonds_double_bonds/output/LOG.ref @@ -42,11 +42,6 @@ R(c!1),R(c!1) => v R(c!1,cr),R(c!1,cr) v R(c!1,cr),R(c!1,cr!R.n) ] -R(c!1),R(c!1) => - [ - R(c!1,cr!R.n),R(c!1,n!R.cr) - v R(c!1,cr),R(c!1,n) - ] R(c!1),R(c!1) => [ R(c!1,n!R.cr),R(c!1,n) diff --git a/models/test_suite/CMSB_paper/sos/output/LOG.ref b/models/test_suite/CMSB_paper/sos/output/LOG.ref index c357504236..77d1f104f9 100644 --- a/models/test_suite/CMSB_paper/sos/output/LOG.ref +++ b/models/test_suite/CMSB_paper/sos/output/LOG.ref @@ -18,9 +18,9 @@ every agent may occur in the model EGF() => [ EGF(r) v EGF(r!EGFR.L) ] EGFR() => [ EGFR(Y1092~u?) v EGFR(Y1092~p?) ] EGFR() => [ EGFR(Y1172~u?) v EGFR(Y1172~p?) ] -EGFR() => EGFR(Y1016~u) EGFR() => [ EGFR(L) v EGFR(L!EGF.r) ] EGFR() => [ EGFR(CR) v EGFR(CR!EGFR.CR) ] +EGFR() => EGFR(Y1016~u) EGFR() => [ EGFR(N) v EGFR(N!EGFR.C) ] EGFR() => [ EGFR(C) v EGFR(C!EGFR.N) ] EGFR() => [ EGFR(Y1172) v EGFR(Y1172!Shc.PTB) ] @@ -29,8 +29,8 @@ SoS() => [ SoS(PR) v SoS(PR!Grb2.SH3n) ] SoS() => SoS(S~u) Shc() => Shc(PTB~u?) Shc() => [ Shc(Y) v Shc(Y!Grb2.SH2) ] -Shc() => [ Shc(Y~u?) v Shc(Y~p?) ] Shc() => [ Shc(PTB) v Shc(PTB!EGFR.Y1172) ] +Shc() => [ Shc(Y~u?) v Shc(Y~p?) ] Grb2() => [ Grb2(SH2) v Grb2(SH2!Shc.Y) v Grb2(SH2!EGFR.Y1092) ] Grb2() => [ Grb2(SH3n) v Grb2(SH3n!SoS.PR) ] Grb2() => Grb2(SH2~u?) diff --git a/models/test_suite/kasa_preprocessing/abc/output/LOG.ref b/models/test_suite/kasa_preprocessing/abc/output/LOG.ref index f885c6a7b0..d261e886b9 100644 --- a/models/test_suite/kasa_preprocessing/abc/output/LOG.ref +++ b/models/test_suite/kasa_preprocessing/abc/output/LOG.ref @@ -697,12 +697,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(x!,c!) INTENSIONAL DESCRIPTION: -Id=47 +Id=51 Node(site_type:1<1) Id=0 Leaf False - Id=46 + Id=50 Node(site_type:1<2) Id=19 Node(site_type:2<1) @@ -727,26 +727,26 @@ EXTENSIONAL DESCRIPTION: Updating the views for C(x1~,x2~,x1!,x2!) INTENSIONAL DESCRIPTION: -Id=57 +Id=61 Node(site_type:1<0) Id=0 Leaf False - Id=56 + Id=60 Node(site_type:1<1) - Id=55 + Id=59 Node(site_type:2<0) Id=0 Leaf False - Id=54 + Id=58 Node(site_type:2<1) - Id=53 + Id=57 Node(site_type:3<1) Id=0 Leaf False - Id=52 + Id=56 Node(site_type:3<2) Id=23 Node(site_type:4<0) @@ -926,19 +926,19 @@ EXTENSIONAL DESCRIPTION: Updating the views for C(x1~,x2~,x1!,x2!) INTENSIONAL DESCRIPTION: -Id=86 +Id=90 Node(site_type:1<1) Id=0 Leaf False - Id=85 + Id=89 Node(site_type:1<2) - Id=84 + Id=88 Node(site_type:2<1) Id=0 Leaf False - Id=83 + Id=87 Node(site_type:2<2) Id=25 Node(site_type:3<0) @@ -979,12 +979,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(x!,c!) INTENSIONAL DESCRIPTION: -Id=101 +Id=105 Node(site_type:1<1) Id=0 Leaf False - Id=100 + Id=104 Node(site_type:1<2) Id=31 Node(site_type:2<2) @@ -1021,12 +1021,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(x!,c!) INTENSIONAL DESCRIPTION: -Id=64 +Id=68 Node(site_type:1<0) Id=0 Leaf False - Id=63 + Id=67 Node(site_type:1<1) Id=19 Node(site_type:2<1) @@ -1100,14 +1100,14 @@ every agent may occur in the model * Fixpoint iteration : ------------------------------------------------------------ agent_type:0:A:cv_id:0 -Id=115 +Id=118 Node(site_type:1<0) Id=0 Leaf False - Id=97 + Id=101 Node(site_type:1<2) - Id=96 + Id=100 Node(site_type:2<0) Id=0 Leaf False @@ -1138,26 +1138,26 @@ Id=45 Leaf False agent_type:2:C:cv_id:0 -Id=91 +Id=95 Node(site_type:1<0) Id=0 Leaf False - Id=90 + Id=94 Node(site_type:1<1) - Id=60 + Id=64 Node(site_type:2<0) Id=0 Leaf False - Id=59 + Id=63 Node(site_type:2<1) - Id=58 + Id=62 Node(site_type:3<0) Id=0 Leaf False - Id=52 + Id=56 Node(site_type:3<2) Id=23 Node(site_type:4<0) @@ -1178,23 +1178,23 @@ Id=91 Id=0 Leaf False - Id=89 + Id=93 Node(site_type:1<2) - Id=88 + Id=92 Node(site_type:2<0) Id=0 Leaf False - Id=87 + Id=91 Node(site_type:2<1) - Id=75 + Id=79 Node(site_type:3<0) Id=0 Leaf False - Id=74 + Id=78 Node(site_type:3<1) - Id=73 + Id=77 Node(site_type:4<0) Id=0 Leaf False @@ -1210,7 +1210,7 @@ Id=91 Id=0 Leaf False - Id=83 + Id=87 Node(site_type:2<2) Id=25 Node(site_type:3<0) @@ -1246,12 +1246,12 @@ Id=91 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=117 +Id=120 Node(site_type:1<0) Id=0 Leaf False - Id=116 + Id=119 Node(site_type:1<3) Id=1 Leaf True @@ -1266,7 +1266,7 @@ Id=111 Id=0 Leaf False - Id=104 + Id=48 Node(site_type:0<2) Id=1 Leaf True @@ -1281,7 +1281,7 @@ Id=111 Id=0 Leaf False - Id=104 + Id=48 Node(site_type:0<2) Id=1 Leaf True @@ -1306,7 +1306,7 @@ Id=45 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=48 +Id=52 Node(site_type:2<0) Id=0 Leaf False @@ -1321,7 +1321,7 @@ Id=48 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=122 +Id=125 Node(site_type:3<0) Id=0 Leaf False @@ -1341,7 +1341,7 @@ Id=111 Id=0 Leaf False - Id=104 + Id=48 Node(site_type:0<2) Id=1 Leaf True @@ -1362,12 +1362,12 @@ C() => [ C(x1~u?) v C(x1~p?) ] * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=117 +Id=120 Node(site_type:1<0) Id=0 Leaf False - Id=116 + Id=119 Node(site_type:1<3) Id=1 Leaf True @@ -1382,7 +1382,7 @@ Id=111 Id=0 Leaf False - Id=104 + Id=48 Node(site_type:0<2) Id=1 Leaf True @@ -1397,7 +1397,7 @@ Id=111 Id=0 Leaf False - Id=104 + Id=48 Node(site_type:0<2) Id=1 Leaf True @@ -1407,26 +1407,26 @@ Id=111 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=194 +Id=197 Node(site_type:0<0) Id=0 Leaf False - Id=193 + Id=196 Node(site_type:0<1) - Id=186 + Id=189 Node(site_type:1<0) Id=0 Leaf False - Id=185 + Id=188 Node(site_type:1<1) - Id=153 + Id=156 Node(site_type:2<0) Id=0 Leaf False - Id=152 + Id=155 Node(site_type:2<2) Id=11 Node(site_type:3<0) @@ -1447,23 +1447,23 @@ Id=194 Id=0 Leaf False - Id=192 + Id=195 Node(site_type:0<2) - Id=191 + Id=194 Node(site_type:1<0) Id=0 Leaf False - Id=190 + Id=193 Node(site_type:1<1) - Id=151 + Id=154 Node(site_type:2<0) Id=0 Leaf False - Id=150 + Id=153 Node(site_type:2<1) - Id=122 + Id=125 Node(site_type:3<0) Id=0 Leaf False @@ -1479,14 +1479,14 @@ Id=194 Id=0 Leaf False - Id=189 + Id=192 Node(site_type:1<2) - Id=188 + Id=191 Node(site_type:2<0) Id=0 Leaf False - Id=187 + Id=190 Node(site_type:2<1) Id=11 Node(site_type:3<0) @@ -1526,12 +1526,12 @@ C() => * Properties of pairs of bonds ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=117 +Id=120 Node(site_type:1<0) Id=0 Leaf False - Id=116 + Id=119 Node(site_type:1<3) Id=1 Leaf True @@ -1546,7 +1546,7 @@ Id=111 Id=0 Leaf False - Id=104 + Id=48 Node(site_type:0<2) Id=1 Leaf True @@ -1561,7 +1561,7 @@ Id=111 Id=0 Leaf False - Id=104 + Id=48 Node(site_type:0<2) Id=1 Leaf True @@ -1586,7 +1586,7 @@ Id=45 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=48 +Id=52 Node(site_type:2<0) Id=0 Leaf False @@ -1601,7 +1601,7 @@ Id=48 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=122 +Id=125 Node(site_type:3<0) Id=0 Leaf False @@ -1621,7 +1621,7 @@ Id=111 Id=0 Leaf False - Id=104 + Id=48 Node(site_type:0<2) Id=1 Leaf True @@ -1631,12 +1631,12 @@ Id=111 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=117 +Id=120 Node(site_type:1<0) Id=0 Leaf False - Id=116 + Id=119 Node(site_type:1<3) Id=1 Leaf True @@ -1651,7 +1651,7 @@ Id=111 Id=0 Leaf False - Id=104 + Id=48 Node(site_type:0<2) Id=1 Leaf True @@ -1666,7 +1666,7 @@ Id=111 Id=0 Leaf False - Id=104 + Id=48 Node(site_type:0<2) Id=1 Leaf True @@ -1676,26 +1676,26 @@ Id=111 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=194 +Id=197 Node(site_type:0<0) Id=0 Leaf False - Id=193 + Id=196 Node(site_type:0<1) - Id=186 + Id=189 Node(site_type:1<0) Id=0 Leaf False - Id=185 + Id=188 Node(site_type:1<1) - Id=153 + Id=156 Node(site_type:2<0) Id=0 Leaf False - Id=152 + Id=155 Node(site_type:2<2) Id=11 Node(site_type:3<0) @@ -1716,23 +1716,23 @@ Id=194 Id=0 Leaf False - Id=192 + Id=195 Node(site_type:0<2) - Id=191 + Id=194 Node(site_type:1<0) Id=0 Leaf False - Id=190 + Id=193 Node(site_type:1<1) - Id=151 + Id=154 Node(site_type:2<0) Id=0 Leaf False - Id=150 + Id=153 Node(site_type:2<1) - Id=122 + Id=125 Node(site_type:3<0) Id=0 Leaf False @@ -1748,14 +1748,14 @@ Id=194 Id=0 Leaf False - Id=189 + Id=192 Node(site_type:1<2) - Id=188 + Id=191 Node(site_type:2<0) Id=0 Leaf False - Id=187 + Id=190 Node(site_type:2<1) Id=11 Node(site_type:3<0) diff --git a/models/test_suite/reachability_analysis/atomic_parallel_bonds/output/LOG.ref b/models/test_suite/reachability_analysis/atomic_parallel_bonds/output/LOG.ref index 87d14e883a..e1cc02746a 100644 --- a/models/test_suite/reachability_analysis/atomic_parallel_bonds/output/LOG.ref +++ b/models/test_suite/reachability_analysis/atomic_parallel_bonds/output/LOG.ref @@ -366,7 +366,7 @@ Id=15 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=18 +Id=20 Node(site_type:1<0) Id=0 Leaf False @@ -381,12 +381,12 @@ Id=18 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=21 +Id=23 Node(site_type:0<0) Id=0 Leaf False - Id=20 + Id=22 Node(site_type:0<2) Id=1 Leaf True @@ -396,7 +396,7 @@ Id=21 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=18 +Id=20 Node(site_type:1<0) Id=0 Leaf False @@ -411,12 +411,12 @@ Id=18 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=21 +Id=23 Node(site_type:0<0) Id=0 Leaf False - Id=20 + Id=22 Node(site_type:0<2) Id=1 Leaf True @@ -434,12 +434,12 @@ B() => [ B(z) v B(z!A.z) ] * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=26 +Id=28 Node(site_type:0<0) Id=0 Leaf False - Id=25 + Id=27 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -454,7 +454,7 @@ Id=26 Id=0 Leaf False - Id=24 + Id=26 Node(site_type:0<2) Id=17 Node(site_type:1<1) @@ -474,12 +474,12 @@ Id=26 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=26 +Id=28 Node(site_type:0<0) Id=0 Leaf False - Id=25 + Id=27 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -494,7 +494,7 @@ Id=26 Id=0 Leaf False - Id=24 + Id=26 Node(site_type:0<2) Id=17 Node(site_type:1<1) @@ -524,7 +524,7 @@ B(z!A.z) <=> B(t!A.t) A(t!B.t,z!B.z) => A(t!2,z!1),B(t!2,z!1) B(t!A.t,z!A.z) => B(t!2,z!1),A(t!2,z!1) INTENSIONAL DESCRIPTION: -Id=18 +Id=20 Node(site_type:1<0) Id=0 Leaf False @@ -539,12 +539,12 @@ Id=18 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=21 +Id=23 Node(site_type:0<0) Id=0 Leaf False - Id=20 + Id=22 Node(site_type:0<2) Id=1 Leaf True @@ -554,7 +554,7 @@ Id=21 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=18 +Id=20 Node(site_type:1<0) Id=0 Leaf False @@ -569,12 +569,12 @@ Id=18 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=21 +Id=23 Node(site_type:0<0) Id=0 Leaf False - Id=20 + Id=22 Node(site_type:0<2) Id=1 Leaf True @@ -584,12 +584,12 @@ Id=21 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=26 +Id=28 Node(site_type:0<0) Id=0 Leaf False - Id=25 + Id=27 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -604,7 +604,7 @@ Id=26 Id=0 Leaf False - Id=24 + Id=26 Node(site_type:0<2) Id=17 Node(site_type:1<1) @@ -624,12 +624,12 @@ Id=26 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=26 +Id=28 Node(site_type:0<0) Id=0 Leaf False - Id=25 + Id=27 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -644,7 +644,7 @@ Id=26 Id=0 Leaf False - Id=24 + Id=26 Node(site_type:0<2) Id=17 Node(site_type:1<1) diff --git a/models/test_suite/reachability_analysis/low_res_contact_map/output/LOG.ref b/models/test_suite/reachability_analysis/low_res_contact_map/output/LOG.ref index b192a18084..2ecba39ab4 100644 --- a/models/test_suite/reachability_analysis/low_res_contact_map/output/LOG.ref +++ b/models/test_suite/reachability_analysis/low_res_contact_map/output/LOG.ref @@ -21,8 +21,8 @@ C cannot occur in the model * Non relational properties: ------------------------------------------------------------ A() => [ A(z~u?) v A(z~p?) ] -A() => [ A(y~u?) v A(y~p?) ] A() => A(z) +A() => [ A(y~u?) v A(y~p?) ] A() => A(y) ------------------------------------------------------------ diff --git a/models/test_suite/reachability_analysis/medium_res_contact_map/output/LOG.ref b/models/test_suite/reachability_analysis/medium_res_contact_map/output/LOG.ref index e8de0ca8fd..51edcc05a2 100644 --- a/models/test_suite/reachability_analysis/medium_res_contact_map/output/LOG.ref +++ b/models/test_suite/reachability_analysis/medium_res_contact_map/output/LOG.ref @@ -20,8 +20,8 @@ C cannot occur in the model * Non relational properties: ------------------------------------------------------------ A() => [ A(z~u?) v A(z~p?) ] -A() => [ A(y~u?) v A(y~p?) ] A() => A(z) +A() => [ A(y~u?) v A(y~p?) ] A() => A(y) ------------------------------------------------------------ diff --git a/models/test_suite/reachability_analysis/parallel_bond_precondition1/output/LOG.ref b/models/test_suite/reachability_analysis/parallel_bond_precondition1/output/LOG.ref index 21bfe92589..546d030d05 100644 --- a/models/test_suite/reachability_analysis/parallel_bond_precondition1/output/LOG.ref +++ b/models/test_suite/reachability_analysis/parallel_bond_precondition1/output/LOG.ref @@ -711,7 +711,7 @@ every agent may occur in the model * Fixpoint iteration : ------------------------------------------------------------ agent_type:0:A:cv_id:0 -Id=26 +Id=28 Node(site_type:1<0) Id=0 Leaf False @@ -749,7 +749,7 @@ Id=3 Leaf False agent_type:1:B:cv_id:0 -Id=26 +Id=28 Node(site_type:1<0) Id=0 Leaf False @@ -791,13 +791,13 @@ Id=3 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=17 - Node(site_type:2<0) +Id=31 + Node(site_type:1<0) Id=0 Leaf False - Id=12 - Node(site_type:2<2) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -806,13 +806,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=17 + Node(site_type:2<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=12 + Node(site_type:2<2) Id=1 Leaf True @@ -821,12 +821,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:0<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:0<1) Id=1 Leaf True @@ -836,13 +836,13 @@ Id=31 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=17 - Node(site_type:2<0) +Id=31 + Node(site_type:1<0) Id=0 Leaf False - Id=12 - Node(site_type:2<2) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -851,13 +851,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=17 + Node(site_type:2<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=12 + Node(site_type:2<2) Id=1 Leaf True @@ -866,12 +866,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:0<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:0<1) Id=1 Leaf True @@ -880,24 +880,24 @@ Id=31 Leaf False EXTENSIONAL DESCRIPTION: -A() => [ A(t) v A(t!B.t) ] A() => [ A(z) v A(z!B.z) ] +A() => [ A(t) v A(t!B.t) ] A() => A(x~u) -B() => [ B(t) v B(t!A.t) ] B() => [ B(z) v B(z!A.z) ] +B() => [ B(t) v B(t!A.t) ] B() => B(x~u) ------------------------------------------------------------ * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=17 - Node(site_type:2<0) +Id=31 + Node(site_type:1<0) Id=0 Leaf False - Id=12 - Node(site_type:2<2) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -906,13 +906,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=17 + Node(site_type:2<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=12 + Node(site_type:2<2) Id=1 Leaf True @@ -921,12 +921,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:0<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:0<1) Id=1 Leaf True @@ -936,13 +936,13 @@ Id=31 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=17 - Node(site_type:2<0) +Id=31 + Node(site_type:1<0) Id=0 Leaf False - Id=12 - Node(site_type:2<2) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -951,13 +951,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=17 + Node(site_type:2<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=12 + Node(site_type:2<2) Id=1 Leaf True @@ -966,12 +966,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:0<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:0<1) Id=1 Leaf True @@ -994,6 +994,21 @@ A(t!1),B(t!1) => A(t!B.t,z!B.z) => A(t!2,z!1),B(z!1),B(t!2) B(t!A.t,z!A.z) => B(t!2,z!1),A(z!1),A(t!2) INTENSIONAL DESCRIPTION: +Id=31 + Node(site_type:1<0) + Id=0 + Leaf False + + Id=8 + Node(site_type:1<2) + Id=1 + Leaf True + + Id=0 + Leaf False + +EXTENSIONAL DESCRIPTION: +INTENSIONAL DESCRIPTION: Id=17 Node(site_type:2<0) Id=0 @@ -1009,13 +1024,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=33 + Node(site_type:0<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=32 + Node(site_type:0<1) Id=1 Leaf True @@ -1025,12 +1040,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: Id=31 - Node(site_type:0<0) + Node(site_type:1<0) Id=0 Leaf False - Id=30 - Node(site_type:0<1) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -1054,13 +1069,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=33 + Node(site_type:0<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=32 + Node(site_type:0<1) Id=1 Leaf True @@ -1070,12 +1085,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: Id=31 - Node(site_type:0<0) + Node(site_type:1<0) Id=0 Leaf False - Id=30 - Node(site_type:0<1) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -1099,13 +1114,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=33 + Node(site_type:0<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=32 + Node(site_type:0<1) Id=1 Leaf True @@ -1115,12 +1130,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: Id=31 - Node(site_type:0<0) + Node(site_type:1<0) Id=0 Leaf False - Id=30 - Node(site_type:0<1) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -1144,27 +1159,12 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) - Id=0 - Leaf False - - Id=8 - Node(site_type:1<2) - Id=1 - Leaf True - - Id=0 - Leaf False - -EXTENSIONAL DESCRIPTION: -INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:0<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:0<1) Id=1 Leaf True @@ -1177,19 +1177,19 @@ EXTENSIONAL DESCRIPTION: * Export Views domain - non relational properties to JSon (internal constraints_list): ------------------------------------------------------------ B()=> [B(x~u)] -B()=> [ - B(z) - v B(z!A.z)] B()=> [ B(t) v B(t!A.t)] +B()=> [ + B(z) + v B(z!A.z)] A()=> [A(x~u)] -A()=> [ - A(z) - v A(z!B.z)] A()=> [ A(t) v A(t!B.t)] +A()=> [ + A(z) + v A(z!B.z)] ------------------------------------------------------------ * Export Views domain - relational properties to JSon (internal constraints_list): diff --git a/models/test_suite/reachability_analysis/parallel_bond_precondition2/output/LOG.ref b/models/test_suite/reachability_analysis/parallel_bond_precondition2/output/LOG.ref index 19a6971121..0f40a70557 100644 --- a/models/test_suite/reachability_analysis/parallel_bond_precondition2/output/LOG.ref +++ b/models/test_suite/reachability_analysis/parallel_bond_precondition2/output/LOG.ref @@ -671,7 +671,7 @@ every agent may occur in the model * Fixpoint iteration : ------------------------------------------------------------ agent_type:0:A:cv_id:0 -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -709,7 +709,7 @@ Id=3 Leaf False agent_type:1:B:cv_id:0 -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -751,13 +751,13 @@ Id=3 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=17 - Node(site_type:2<0) +Id=31 + Node(site_type:1<0) Id=0 Leaf False - Id=12 - Node(site_type:2<2) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -766,13 +766,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=17 + Node(site_type:2<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=12 + Node(site_type:2<2) Id=1 Leaf True @@ -781,12 +781,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:0<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:0<1) Id=1 Leaf True @@ -796,13 +796,13 @@ Id=31 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=17 - Node(site_type:2<0) +Id=31 + Node(site_type:1<0) Id=0 Leaf False - Id=12 - Node(site_type:2<2) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -811,13 +811,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=17 + Node(site_type:2<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=12 + Node(site_type:2<2) Id=1 Leaf True @@ -826,12 +826,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:0<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:0<1) Id=1 Leaf True @@ -840,24 +840,24 @@ Id=31 Leaf False EXTENSIONAL DESCRIPTION: -A() => [ A(t) v A(t!B.t) ] A() => [ A(z) v A(z!B.z) ] +A() => [ A(t) v A(t!B.t) ] A() => A(x~u) -B() => [ B(t) v B(t!A.t) ] B() => [ B(z) v B(z!A.z) ] +B() => [ B(t) v B(t!A.t) ] B() => B(x~u) ------------------------------------------------------------ * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=17 - Node(site_type:2<0) +Id=31 + Node(site_type:1<0) Id=0 Leaf False - Id=12 - Node(site_type:2<2) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -866,13 +866,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=17 + Node(site_type:2<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=12 + Node(site_type:2<2) Id=1 Leaf True @@ -881,12 +881,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:0<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:0<1) Id=1 Leaf True @@ -896,13 +896,13 @@ Id=31 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=17 - Node(site_type:2<0) +Id=31 + Node(site_type:1<0) Id=0 Leaf False - Id=12 - Node(site_type:2<2) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -911,13 +911,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=17 + Node(site_type:2<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=12 + Node(site_type:2<2) Id=1 Leaf True @@ -926,12 +926,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:0<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:0<1) Id=1 Leaf True @@ -954,6 +954,21 @@ A(t!1),B(t!1) => A(t!B.t,z!B.z) => A(t!2,z!1),B(z!1),B(t!2) B(t!A.t,z!A.z) => B(t!2,z!1),A(z!1),A(t!2) INTENSIONAL DESCRIPTION: +Id=31 + Node(site_type:1<0) + Id=0 + Leaf False + + Id=8 + Node(site_type:1<2) + Id=1 + Leaf True + + Id=0 + Leaf False + +EXTENSIONAL DESCRIPTION: +INTENSIONAL DESCRIPTION: Id=17 Node(site_type:2<0) Id=0 @@ -969,13 +984,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=33 + Node(site_type:0<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=32 + Node(site_type:0<1) Id=1 Leaf True @@ -985,12 +1000,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: Id=31 - Node(site_type:0<0) + Node(site_type:1<0) Id=0 Leaf False - Id=30 - Node(site_type:0<1) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -1014,13 +1029,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=33 + Node(site_type:0<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=32 + Node(site_type:0<1) Id=1 Leaf True @@ -1030,12 +1045,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: Id=31 - Node(site_type:0<0) + Node(site_type:1<0) Id=0 Leaf False - Id=30 - Node(site_type:0<1) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -1059,13 +1074,13 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) +Id=33 + Node(site_type:0<0) Id=0 Leaf False - Id=8 - Node(site_type:1<2) + Id=32 + Node(site_type:0<1) Id=1 Leaf True @@ -1075,12 +1090,12 @@ Id=29 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: Id=31 - Node(site_type:0<0) + Node(site_type:1<0) Id=0 Leaf False - Id=30 - Node(site_type:0<1) + Id=8 + Node(site_type:1<2) Id=1 Leaf True @@ -1104,27 +1119,12 @@ Id=17 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=29 - Node(site_type:1<0) - Id=0 - Leaf False - - Id=8 - Node(site_type:1<2) - Id=1 - Leaf True - - Id=0 - Leaf False - -EXTENSIONAL DESCRIPTION: -INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:0<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:0<1) Id=1 Leaf True @@ -1137,19 +1137,19 @@ EXTENSIONAL DESCRIPTION: * Export Views domain - non relational properties to JSon (internal constraints_list): ------------------------------------------------------------ B()=> [B(x~u)] -B()=> [ - B(z) - v B(z!A.z)] B()=> [ B(t) v B(t!A.t)] +B()=> [ + B(z) + v B(z!A.z)] A()=> [A(x~u)] -A()=> [ - A(z) - v A(z!B.z)] A()=> [ A(t) v A(t!B.t)] +A()=> [ + A(z) + v A(z!B.z)] ------------------------------------------------------------ * Export Views domain - relational properties to JSon (internal constraints_list): diff --git a/models/test_suite/reachability_analysis/parallel_bonds_complex_init_maybe/output/LOG.ref b/models/test_suite/reachability_analysis/parallel_bonds_complex_init_maybe/output/LOG.ref index cd06b937ef..21f9223eae 100644 --- a/models/test_suite/reachability_analysis/parallel_bonds_complex_init_maybe/output/LOG.ref +++ b/models/test_suite/reachability_analysis/parallel_bonds_complex_init_maybe/output/LOG.ref @@ -595,12 +595,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(x~,z!,t!) INTENSIONAL DESCRIPTION: -Id=26 +Id=28 Node(site_type:1<0) Id=0 Leaf False - Id=25 + Id=27 Node(site_type:1<2) Id=17 Node(site_type:2<0) @@ -636,12 +636,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for B(x~,z!,t!) INTENSIONAL DESCRIPTION: -Id=33 +Id=35 Node(site_type:1<0) Id=0 Leaf False - Id=32 + Id=34 Node(site_type:1<1) Id=17 Node(site_type:2<0) @@ -791,7 +791,7 @@ Id=70 Id=44 Node(site_type:2<1) - Id=27 + Id=29 Node(site_type:3<0) Id=0 Leaf False @@ -851,12 +851,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(x~,z!,t!) INTENSIONAL DESCRIPTION: -Id=72 +Id=78 Node(site_type:1<1) Id=0 Leaf False - Id=71 + Id=77 Node(site_type:1<2) Id=21 Node(site_type:2<1) @@ -891,12 +891,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for B(x~,z!,t!) INTENSIONAL DESCRIPTION: -Id=72 +Id=78 Node(site_type:1<1) Id=0 Leaf False - Id=71 + Id=77 Node(site_type:1<2) Id=21 Node(site_type:2<1) @@ -1061,16 +1061,16 @@ EXTENSIONAL DESCRIPTION: Updating the views for B(x~,z!,t!) - Applying rule r4 (File "parallel_bonds.ka", line 11, characters 4-50:): + Applying rule r1 (File "parallel_bonds.ka", line 8, characters 4-24:): the precondition is satisfied - Updating the views for A(x~,z!,t!) - Updating the views for B(x~,z!,t!) - Applying rule r1 (File "parallel_bonds.ka", line 8, characters 4-24:): + Applying rule r4 (File "parallel_bonds.ka", line 11, characters 4-50:): the precondition is satisfied + Updating the views for A(x~,z!,t!) + Updating the views for B(x~,z!,t!) Applying rule r5 (File "parallel_bonds.ka", line 12, characters 4-50:): @@ -1110,16 +1110,16 @@ Id=102 Id=0 Leaf False - Id=75 + Id=81 Node(site_type:1<2) - Id=74 + Id=80 Node(site_type:2<0) Id=0 Leaf False - Id=73 + Id=79 Node(site_type:2<2) - Id=27 + Id=29 Node(site_type:3<0) Id=0 Leaf False @@ -1144,16 +1144,16 @@ Id=102 Id=0 Leaf False - Id=75 + Id=81 Node(site_type:1<2) - Id=74 + Id=80 Node(site_type:2<0) Id=0 Leaf False - Id=73 + Id=79 Node(site_type:2<2) - Id=27 + Id=29 Node(site_type:3<0) Id=0 Leaf False @@ -1369,23 +1369,6 @@ EXTENSIONAL DESCRIPTION: ------------------------------------------------------------ * Properties in connected agents ------------------------------------------------------------ -A(z!1),B(z!1) => - [ - A(x~p,z!1),B(t,z!1) - v A(x~p,z!1),B(t!A.t,z!1) - v A(x~u,z!1),B(t!A.t,z!1) - ] -A(z!1),B(z!1) => - [ - A(t!B.t,z!1),B(x~u,z!1) - v A(t!B.t,z!1),B(x~p,z!1) - v A(t,z!1),B(x~p,z!1) - ] -A(z!1),B(z!1) => - [ - A(t!B.t,z!1),B(t!A.t,z!1) - v A(t,z!1),B(t,z!1) - ] ------------------------------------------------------------ * Properties of pairs of bonds ------------------------------------------------------------ @@ -1600,17 +1583,6 @@ A()=> [ ------------------------------------------------------------ * Export Connected agents to JSon (internal constraints_list): ------------------------------------------------------------ -A(z!1),B(z!1)=> [ - A(x~p,z!1),B(t,z!1) - v A(x~p,z!1),B(t!A.t,z!1) - v A(x~u,z!1),B(t!A.t,z!1)] -A(z!1),B(z!1)=> [ - A(t!B.t,z!1),B(x~u,z!1) - v A(t!B.t,z!1),B(x~p,z!1) - v A(t,z!1),B(x~p,z!1)] -A(z!1),B(z!1)=> [ - A(t!B.t,z!1),B(t!A.t,z!1) - v A(t,z!1),B(t,z!1)] ------------------------------------------------------------ * Export Parallel bonds to JSon (internal constraints_list): diff --git a/models/test_suite/reachability_analysis/parallel_bonds_complex_init_yes/output/LOG.ref b/models/test_suite/reachability_analysis/parallel_bonds_complex_init_yes/output/LOG.ref index 76c49c7201..60725bd87e 100644 --- a/models/test_suite/reachability_analysis/parallel_bonds_complex_init_yes/output/LOG.ref +++ b/models/test_suite/reachability_analysis/parallel_bonds_complex_init_yes/output/LOG.ref @@ -612,12 +612,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(x~,z!,t!) INTENSIONAL DESCRIPTION: -Id=30 +Id=32 Node(site_type:1<0) Id=0 Leaf False - Id=29 + Id=31 Node(site_type:1<1) Id=19 Node(site_type:2<0) @@ -652,12 +652,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for B(x~,z!,t!) INTENSIONAL DESCRIPTION: -Id=30 +Id=32 Node(site_type:1<0) Id=0 Leaf False - Id=29 + Id=31 Node(site_type:1<1) Id=19 Node(site_type:2<0) @@ -792,12 +792,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for B(x~,z!,t!) INTENSIONAL DESCRIPTION: -Id=62 +Id=64 Node(site_type:1<1) Id=0 Leaf False - Id=61 + Id=63 Node(site_type:1<2) Id=47 Node(site_type:2<0) @@ -806,7 +806,7 @@ Id=62 Id=46 Node(site_type:2<1) - Id=31 + Id=33 Node(site_type:3<0) Id=0 Leaf False @@ -859,14 +859,14 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(x~,z!,t!) INTENSIONAL DESCRIPTION: -Id=72 +Id=74 Node(site_type:1<1) Id=0 Leaf False - Id=71 + Id=73 Node(site_type:1<2) - Id=58 + Id=60 Node(site_type:2<0) Id=0 Leaf False @@ -905,12 +905,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(x~,z!,t!) INTENSIONAL DESCRIPTION: -Id=80 +Id=86 Node(site_type:1<1) Id=0 Leaf False - Id=79 + Id=85 Node(site_type:1<2) Id=23 Node(site_type:2<1) @@ -945,12 +945,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for B(x~,z!,t!) INTENSIONAL DESCRIPTION: -Id=80 +Id=86 Node(site_type:1<1) Id=0 Leaf False - Id=79 + Id=85 Node(site_type:1<2) Id=23 Node(site_type:2<1) @@ -1077,16 +1077,16 @@ EXTENSIONAL DESCRIPTION: Updating the views for B(x~,z!,t!) - Applying rule r4 (File "parallel_bonds.ka", line 11, characters 4-50:): + Applying rule r1 (File "parallel_bonds.ka", line 8, characters 4-24:): the precondition is satisfied - Updating the views for A(x~,z!,t!) - Updating the views for B(x~,z!,t!) - Applying rule r1 (File "parallel_bonds.ka", line 8, characters 4-24:): + Applying rule r4 (File "parallel_bonds.ka", line 11, characters 4-50:): the precondition is satisfied + Updating the views for A(x~,z!,t!) + Updating the views for B(x~,z!,t!) Applying rule r5 (File "parallel_bonds.ka", line 12, characters 4-50:): @@ -1124,25 +1124,6 @@ EXTENSIONAL DESCRIPTION: the precondition is satisfied Updating the views for A(x~,z!,t!) - - Applying rule r1 (File "parallel_bonds.ka", line 8, characters 4-24:): - the precondition is satisfied - - Updating the views for B(x~,z!,t!) - - Applying rule r4 (File "parallel_bonds.ka", line 11, characters 4-50:): - the precondition is satisfied - - Updating the views for A(x~,z!,t!) - - Updating the views for B(x~,z!,t!) - - Applying rule r5 (File "parallel_bonds.ka", line 12, characters 4-50:): - the precondition is satisfied - - Updating the views for A(x~,z!,t!) - - Updating the views for B(x~,z!,t!) ------------------------------------------------------------ every rule may be applied ------------------------------------------------------------ @@ -1152,12 +1133,12 @@ every agent may occur in the model * Fixpoint iteration : ------------------------------------------------------------ agent_type:0:A:cv_id:0 -Id=85 +Id=91 Node(site_type:1<0) Id=0 Leaf False - Id=84 + Id=90 Node(site_type:1<1) Id=47 Node(site_type:2<0) @@ -1166,7 +1147,7 @@ Id=85 Id=46 Node(site_type:2<1) - Id=31 + Id=33 Node(site_type:3<0) Id=0 Leaf False @@ -1197,16 +1178,16 @@ Id=85 Id=0 Leaf False - Id=83 + Id=89 Node(site_type:1<2) - Id=82 + Id=88 Node(site_type:2<0) Id=0 Leaf False - Id=81 + Id=87 Node(site_type:2<2) - Id=31 + Id=33 Node(site_type:3<0) Id=0 Leaf False @@ -1231,16 +1212,16 @@ Id=106 Id=0 Leaf False - Id=83 + Id=89 Node(site_type:1<2) - Id=82 + Id=88 Node(site_type:2<0) Id=0 Leaf False - Id=81 + Id=87 Node(site_type:2<2) - Id=31 + Id=33 Node(site_type:3<0) Id=0 Leaf False @@ -1264,7 +1245,7 @@ Id=106 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=75 +Id=77 Node(site_type:1<0) Id=0 Leaf False @@ -1279,7 +1260,7 @@ Id=75 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=66 +Id=68 Node(site_type:2<0) Id=0 Leaf False @@ -1294,12 +1275,12 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=77 +Id=78 Node(site_type:0<0) Id=0 Leaf False - Id=76 + Id=58 Node(site_type:0<2) Id=1 Leaf True @@ -1309,7 +1290,7 @@ Id=77 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=77 Node(site_type:1<0) Id=0 Leaf False @@ -1324,7 +1305,7 @@ Id=75 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=66 +Id=68 Node(site_type:2<0) Id=0 Leaf False @@ -1339,12 +1320,12 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=77 +Id=78 Node(site_type:0<0) Id=0 Leaf False - Id=76 + Id=58 Node(site_type:0<2) Id=1 Leaf True @@ -1371,14 +1352,14 @@ Id=118 Id=117 Node(site_type:0<1) - Id=87 + Id=80 Node(site_type:1<0) Id=0 Leaf False - Id=86 + Id=79 Node(site_type:1<1) - Id=66 + Id=68 Node(site_type:2<0) Id=0 Leaf False @@ -1391,7 +1372,7 @@ Id=118 Id=0 Leaf False - Id=40 + Id=54 Node(site_type:1<2) Id=21 Node(site_type:2<1) @@ -1411,14 +1392,14 @@ Id=118 Id=116 Node(site_type:0<2) - Id=98 + Id=81 Node(site_type:1<0) Id=0 Leaf False - Id=69 + Id=71 Node(site_type:1<2) - Id=66 + Id=68 Node(site_type:2<0) Id=0 Leaf False @@ -1439,7 +1420,7 @@ Id=118 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=77 Node(site_type:1<0) Id=0 Leaf False @@ -1454,7 +1435,7 @@ Id=75 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=66 +Id=68 Node(site_type:2<0) Id=0 Leaf False @@ -1469,12 +1450,12 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=77 +Id=78 Node(site_type:0<0) Id=0 Leaf False - Id=76 + Id=58 Node(site_type:0<2) Id=1 Leaf True @@ -1502,17 +1483,6 @@ A(z!1),B(z!1) => v A(x~p,z!1),B(t!A.t,z!1) v A(x~u,z!1),B(t!A.t,z!1) ] -A(z!1),B(z!1) => - [ - A(t!B.t,z!1),B(x~u,z!1) - v A(t!B.t,z!1),B(x~p,z!1) - v A(t,z!1),B(x~p,z!1) - ] -A(z!1),B(z!1) => - [ - A(t!B.t,z!1),B(t!A.t,z!1) - v A(t,z!1),B(t,z!1) - ] A(t!1),B(t!1) => [ A(t!1,z!B.z),B(t!1,z!A.z) @@ -1525,7 +1495,7 @@ A(t!1),B(t!1) => A(t!B.t,z!B.z) => A(t!2,z!1),B(t!2,z!1) INTENSIONAL DESCRIPTION: -Id=75 +Id=77 Node(site_type:1<0) Id=0 Leaf False @@ -1540,7 +1510,7 @@ Id=75 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=66 +Id=68 Node(site_type:2<0) Id=0 Leaf False @@ -1555,12 +1525,12 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=77 +Id=78 Node(site_type:0<0) Id=0 Leaf False - Id=76 + Id=58 Node(site_type:0<2) Id=1 Leaf True @@ -1570,7 +1540,7 @@ Id=77 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=77 Node(site_type:1<0) Id=0 Leaf False @@ -1585,7 +1555,7 @@ Id=75 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=66 +Id=68 Node(site_type:2<0) Id=0 Leaf False @@ -1600,12 +1570,12 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=77 +Id=78 Node(site_type:0<0) Id=0 Leaf False - Id=76 + Id=58 Node(site_type:0<2) Id=1 Leaf True @@ -1622,14 +1592,14 @@ Id=118 Id=117 Node(site_type:0<1) - Id=87 + Id=80 Node(site_type:1<0) Id=0 Leaf False - Id=86 + Id=79 Node(site_type:1<1) - Id=66 + Id=68 Node(site_type:2<0) Id=0 Leaf False @@ -1642,7 +1612,7 @@ Id=118 Id=0 Leaf False - Id=40 + Id=54 Node(site_type:1<2) Id=21 Node(site_type:2<1) @@ -1662,14 +1632,14 @@ Id=118 Id=116 Node(site_type:0<2) - Id=98 + Id=81 Node(site_type:1<0) Id=0 Leaf False - Id=69 + Id=71 Node(site_type:1<2) - Id=66 + Id=68 Node(site_type:2<0) Id=0 Leaf False @@ -1690,7 +1660,7 @@ Id=118 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=77 Node(site_type:1<0) Id=0 Leaf False @@ -1705,7 +1675,7 @@ Id=75 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=66 +Id=68 Node(site_type:2<0) Id=0 Leaf False @@ -1720,12 +1690,12 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=77 +Id=78 Node(site_type:0<0) Id=0 Leaf False - Id=76 + Id=58 Node(site_type:0<2) Id=1 Leaf True @@ -1789,13 +1759,6 @@ A(z!1),B(z!1)=> [ A(x~p,z!1),B(t,z!1) v A(x~p,z!1),B(t!A.t,z!1) v A(x~u,z!1),B(t!A.t,z!1)] -A(z!1),B(z!1)=> [ - A(t!B.t,z!1),B(x~u,z!1) - v A(t!B.t,z!1),B(x~p,z!1) - v A(t,z!1),B(x~p,z!1)] -A(z!1),B(z!1)=> [ - A(t!B.t,z!1),B(t!A.t,z!1) - v A(t,z!1),B(t,z!1)] A(t!1),B(t!1)=> [ A(t!1,z!B.z),B(t!1,z!A.z) v A(t!1,z),B(t!1,z) diff --git a/models/test_suite/reachability_analysis/parallel_bonds_init_maybe/output/LOG.ref b/models/test_suite/reachability_analysis/parallel_bonds_init_maybe/output/LOG.ref index eb77cbd001..92be81f3f5 100644 --- a/models/test_suite/reachability_analysis/parallel_bonds_init_maybe/output/LOG.ref +++ b/models/test_suite/reachability_analysis/parallel_bonds_init_maybe/output/LOG.ref @@ -642,7 +642,7 @@ every agent may occur in the model * Fixpoint iteration : ------------------------------------------------------------ agent_type:0:A:cv_id:0 -Id=29 +Id=31 Node(site_type:1<0) Id=0 Leaf False @@ -666,7 +666,7 @@ Id=29 Leaf False agent_type:1:B:cv_id:0 -Id=29 +Id=31 Node(site_type:1<0) Id=0 Leaf False @@ -694,7 +694,7 @@ Id=29 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=32 +Id=34 Node(site_type:1<0) Id=0 Leaf False @@ -709,12 +709,12 @@ Id=32 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=34 +Id=36 Node(site_type:0<0) Id=0 Leaf False - Id=33 + Id=35 Node(site_type:0<2) Id=1 Leaf True @@ -724,7 +724,7 @@ Id=34 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=32 +Id=34 Node(site_type:1<0) Id=0 Leaf False @@ -739,12 +739,12 @@ Id=32 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=34 +Id=36 Node(site_type:0<0) Id=0 Leaf False - Id=33 + Id=35 Node(site_type:0<2) Id=1 Leaf True @@ -762,7 +762,7 @@ B() => [ B(z) v B(z!A.z) ] * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=32 +Id=34 Node(site_type:1<0) Id=0 Leaf False @@ -777,12 +777,12 @@ Id=32 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=34 +Id=36 Node(site_type:0<0) Id=0 Leaf False - Id=33 + Id=35 Node(site_type:0<2) Id=1 Leaf True @@ -792,7 +792,7 @@ Id=34 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=32 +Id=34 Node(site_type:1<0) Id=0 Leaf False @@ -807,12 +807,12 @@ Id=32 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=34 +Id=36 Node(site_type:0<0) Id=0 Leaf False - Id=33 + Id=35 Node(site_type:0<2) Id=1 Leaf True @@ -842,7 +842,7 @@ A(t!1),B(t!1) => B(t!A.t,z!A.z) => B(t!2,z!1),A(t!2,z!1) INTENSIONAL DESCRIPTION: -Id=32 +Id=34 Node(site_type:1<0) Id=0 Leaf False @@ -857,12 +857,12 @@ Id=32 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=34 +Id=36 Node(site_type:0<0) Id=0 Leaf False - Id=33 + Id=35 Node(site_type:0<2) Id=1 Leaf True @@ -872,7 +872,7 @@ Id=34 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=32 +Id=34 Node(site_type:1<0) Id=0 Leaf False @@ -887,12 +887,12 @@ Id=32 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=34 +Id=36 Node(site_type:0<0) Id=0 Leaf False - Id=33 + Id=35 Node(site_type:0<2) Id=1 Leaf True @@ -902,7 +902,7 @@ Id=34 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=32 +Id=34 Node(site_type:1<0) Id=0 Leaf False @@ -917,12 +917,12 @@ Id=32 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=34 +Id=36 Node(site_type:0<0) Id=0 Leaf False - Id=33 + Id=35 Node(site_type:0<2) Id=1 Leaf True @@ -932,7 +932,7 @@ Id=34 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=32 +Id=34 Node(site_type:1<0) Id=0 Leaf False @@ -947,12 +947,12 @@ Id=32 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=34 +Id=36 Node(site_type:0<0) Id=0 Leaf False - Id=33 + Id=35 Node(site_type:0<2) Id=1 Leaf True diff --git a/models/test_suite/reachability_analysis/parallel_bonds_init_yes/output/LOG.ref b/models/test_suite/reachability_analysis/parallel_bonds_init_yes/output/LOG.ref index 4378d87afd..2a7affce45 100644 --- a/models/test_suite/reachability_analysis/parallel_bonds_init_yes/output/LOG.ref +++ b/models/test_suite/reachability_analysis/parallel_bonds_init_yes/output/LOG.ref @@ -630,7 +630,7 @@ every agent may occur in the model * Fixpoint iteration : ------------------------------------------------------------ agent_type:0:A:cv_id:0 -Id=24 +Id=26 Node(site_type:1<0) Id=0 Leaf False @@ -654,7 +654,7 @@ Id=24 Leaf False agent_type:1:B:cv_id:0 -Id=24 +Id=26 Node(site_type:1<0) Id=0 Leaf False @@ -682,7 +682,7 @@ Id=24 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -697,12 +697,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -712,7 +712,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -727,12 +727,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -750,7 +750,7 @@ B() => [ B(z) v B(z!A.z) ] * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -765,12 +765,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -780,7 +780,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -795,12 +795,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -828,7 +828,7 @@ A(t!1),B(t!1) => A(t!B.t,z!B.z) => A(t!2,z!1),B(t!2,z!1) B(t!A.t,z!A.z) => B(t!2,z!1),A(t!2,z!1) INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -843,12 +843,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -858,7 +858,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -873,12 +873,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -888,7 +888,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -903,12 +903,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -918,7 +918,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -933,12 +933,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True diff --git a/models/test_suite/reachability_analysis/parallel_bonds_only_init_false/output/LOG.ref b/models/test_suite/reachability_analysis/parallel_bonds_only_init_false/output/LOG.ref index 32f8547754..2d1aaf85fc 100644 --- a/models/test_suite/reachability_analysis/parallel_bonds_only_init_false/output/LOG.ref +++ b/models/test_suite/reachability_analysis/parallel_bonds_only_init_false/output/LOG.ref @@ -467,7 +467,7 @@ every agent may occur in the model * Fixpoint iteration : ------------------------------------------------------------ agent_type:0:A:cv_id:0 -Id=27 +Id=29 Node(site_type:1<0) Id=0 Leaf False @@ -534,7 +534,7 @@ Id=23 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=28 +Id=30 Node(site_type:1<0) Id=0 Leaf False @@ -549,12 +549,12 @@ Id=28 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=30 +Id=32 Node(site_type:0<0) Id=0 Leaf False - Id=29 + Id=31 Node(site_type:0<2) Id=1 Leaf True @@ -564,7 +564,7 @@ Id=30 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=28 +Id=30 Node(site_type:1<0) Id=0 Leaf False @@ -579,12 +579,12 @@ Id=28 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=30 +Id=32 Node(site_type:0<0) Id=0 Leaf False - Id=29 + Id=31 Node(site_type:0<2) Id=1 Leaf True @@ -602,7 +602,7 @@ B() => [ B(z) v B(z!A.z) ] * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=28 +Id=30 Node(site_type:1<0) Id=0 Leaf False @@ -617,12 +617,12 @@ Id=28 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=30 +Id=32 Node(site_type:0<0) Id=0 Leaf False - Id=29 + Id=31 Node(site_type:0<2) Id=1 Leaf True @@ -632,14 +632,14 @@ Id=30 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=33 +Id=35 Node(site_type:0<0) Id=0 Leaf False - Id=32 + Id=34 Node(site_type:0<1) - Id=28 + Id=30 Node(site_type:1<0) Id=0 Leaf False @@ -652,7 +652,7 @@ Id=33 Id=0 Leaf False - Id=31 + Id=33 Node(site_type:0<2) Id=3 Node(site_type:1<0) @@ -679,7 +679,7 @@ B(z!A.z) => B(t,z!A.z) * Properties of pairs of bonds ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=28 +Id=30 Node(site_type:1<0) Id=0 Leaf False @@ -694,12 +694,12 @@ Id=28 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=30 +Id=32 Node(site_type:0<0) Id=0 Leaf False - Id=29 + Id=31 Node(site_type:0<2) Id=1 Leaf True @@ -709,7 +709,7 @@ Id=30 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=28 +Id=30 Node(site_type:1<0) Id=0 Leaf False @@ -724,12 +724,12 @@ Id=28 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=30 +Id=32 Node(site_type:0<0) Id=0 Leaf False - Id=29 + Id=31 Node(site_type:0<2) Id=1 Leaf True @@ -739,7 +739,7 @@ Id=30 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=28 +Id=30 Node(site_type:1<0) Id=0 Leaf False @@ -754,12 +754,12 @@ Id=28 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=30 +Id=32 Node(site_type:0<0) Id=0 Leaf False - Id=29 + Id=31 Node(site_type:0<2) Id=1 Leaf True @@ -769,14 +769,14 @@ Id=30 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=33 +Id=35 Node(site_type:0<0) Id=0 Leaf False - Id=32 + Id=34 Node(site_type:0<1) - Id=28 + Id=30 Node(site_type:1<0) Id=0 Leaf False @@ -789,7 +789,7 @@ Id=33 Id=0 Leaf False - Id=31 + Id=33 Node(site_type:0<2) Id=3 Node(site_type:1<0) diff --git a/models/test_suite/reachability_analysis/parallel_bonds_only_init_maybe/output/LOG.ref b/models/test_suite/reachability_analysis/parallel_bonds_only_init_maybe/output/LOG.ref index 0577f565e8..01cc41a467 100644 --- a/models/test_suite/reachability_analysis/parallel_bonds_only_init_maybe/output/LOG.ref +++ b/models/test_suite/reachability_analysis/parallel_bonds_only_init_maybe/output/LOG.ref @@ -542,7 +542,7 @@ Id=24 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -557,12 +557,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -572,7 +572,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -587,12 +587,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -610,7 +610,7 @@ B() => [ B(z) v B(z!A.z) ] * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -625,12 +625,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -640,7 +640,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -655,12 +655,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -686,7 +686,7 @@ A(t!1),B(t!1) => * Properties of pairs of bonds ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -701,12 +701,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -716,7 +716,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -731,12 +731,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -746,7 +746,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -761,12 +761,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -776,7 +776,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -791,12 +791,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True diff --git a/models/test_suite/reachability_analysis/parallel_bonds_only_init_yes/output/LOG.ref b/models/test_suite/reachability_analysis/parallel_bonds_only_init_yes/output/LOG.ref index 27ddb617b3..f58330128e 100644 --- a/models/test_suite/reachability_analysis/parallel_bonds_only_init_yes/output/LOG.ref +++ b/models/test_suite/reachability_analysis/parallel_bonds_only_init_yes/output/LOG.ref @@ -411,12 +411,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(z!,t!) INTENSIONAL DESCRIPTION: -Id=23 +Id=25 Node(site_type:1<0) Id=0 Leaf False - Id=22 + Id=24 Node(site_type:1<1) Id=11 Node(site_type:2<1) @@ -441,12 +441,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for B(z!,t!) INTENSIONAL DESCRIPTION: -Id=23 +Id=25 Node(site_type:1<0) Id=0 Leaf False - Id=22 + Id=24 Node(site_type:1<1) Id=11 Node(site_type:2<1) @@ -496,7 +496,7 @@ every agent may occur in the model * Fixpoint iteration : ------------------------------------------------------------ agent_type:0:A:cv_id:0 -Id=24 +Id=26 Node(site_type:1<0) Id=0 Leaf False @@ -520,7 +520,7 @@ Id=24 Leaf False agent_type:1:B:cv_id:0 -Id=24 +Id=26 Node(site_type:1<0) Id=0 Leaf False @@ -548,7 +548,7 @@ Id=24 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -563,12 +563,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -578,7 +578,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -593,12 +593,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -616,7 +616,7 @@ B() => [ B(z) v B(z!A.z) ] * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -631,12 +631,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -646,7 +646,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -661,12 +661,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -692,7 +692,7 @@ A(t!1),B(t!1) => * Properties of pairs of bonds ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -707,12 +707,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -722,7 +722,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -737,12 +737,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -752,7 +752,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -767,12 +767,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True @@ -782,7 +782,7 @@ Id=27 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=25 +Id=27 Node(site_type:1<0) Id=0 Leaf False @@ -797,12 +797,12 @@ Id=25 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=27 +Id=29 Node(site_type:0<0) Id=0 Leaf False - Id=26 + Id=28 Node(site_type:0<2) Id=1 Leaf True diff --git a/models/test_suite/reachability_analysis/product/output/LOG.ref b/models/test_suite/reachability_analysis/product/output/LOG.ref index bdf1bf1378..e33afe936f 100644 --- a/models/test_suite/reachability_analysis/product/output/LOG.ref +++ b/models/test_suite/reachability_analysis/product/output/LOG.ref @@ -703,19 +703,19 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(z~,z!,t!) INTENSIONAL DESCRIPTION: -Id=36 +Id=40 Node(site_type:1<0) Id=0 Leaf False - Id=35 + Id=39 Node(site_type:1<1) - Id=34 + Id=38 Node(site_type:2<1) Id=0 Leaf False - Id=33 + Id=37 Node(site_type:2<2) Id=19 Node(site_type:3<0) @@ -797,19 +797,19 @@ EXTENSIONAL DESCRIPTION: Updating the views for A(z~,z!,t!) INTENSIONAL DESCRIPTION: -Id=48 +Id=52 Node(site_type:1<1) Id=0 Leaf False - Id=47 + Id=51 Node(site_type:1<2) - Id=34 + Id=38 Node(site_type:2<1) Id=0 Leaf False - Id=33 + Id=37 Node(site_type:2<2) Id=19 Node(site_type:3<0) @@ -943,21 +943,21 @@ every agent may occur in the model * Fixpoint iteration : ------------------------------------------------------------ agent_type:0:A:cv_id:0 -Id=65 +Id=69 Node(site_type:1<0) Id=0 Leaf False - Id=64 + Id=68 Node(site_type:1<2) - Id=44 + Id=48 Node(site_type:2<0) Id=0 Leaf False - Id=43 + Id=47 Node(site_type:2<1) - Id=42 + Id=46 Node(site_type:3<0) Id=0 Leaf False @@ -970,7 +970,7 @@ Id=65 Id=0 Leaf False - Id=33 + Id=37 Node(site_type:2<2) Id=19 Node(site_type:3<0) @@ -996,7 +996,7 @@ Id=65 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=66 +Id=70 Node(site_type:1<0) Id=0 Leaf False @@ -1011,13 +1011,13 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=68 - Node(site_type:0<0) +Id=65 + Node(site_type:2<0) Id=0 Leaf False - Id=67 - Node(site_type:0<2) + Id=4 + Node(site_type:2<2) Id=1 Leaf True @@ -1026,13 +1026,13 @@ Id=68 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=61 - Node(site_type:2<0) +Id=71 + Node(site_type:0<0) Id=0 Leaf False - Id=4 - Node(site_type:2<2) + Id=35 + Node(site_type:0<2) Id=1 Leaf True @@ -1041,19 +1041,19 @@ Id=61 EXTENSIONAL DESCRIPTION: A() => [ A(z) v A(z!A.z) ] -A() => [ A(z~u?) v A(z~p?) ] A() => [ A(t) v A(t!A.t) ] +A() => [ A(z~u?) v A(z~p?) ] ------------------------------------------------------------ * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=68 +Id=71 Node(site_type:0<0) Id=0 Leaf False - Id=67 + Id=35 Node(site_type:0<2) Id=1 Leaf True @@ -1063,14 +1063,14 @@ Id=68 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=72 +Id=75 Node(site_type:1<0) Id=0 Leaf False - Id=71 + Id=74 Node(site_type:1<1) - Id=61 + Id=65 Node(site_type:2<0) Id=0 Leaf False @@ -1083,7 +1083,7 @@ Id=72 Id=0 Leaf False - Id=56 + Id=60 Node(site_type:1<2) Id=17 Node(site_type:2<0) @@ -1120,7 +1120,7 @@ A(t!1),A(t!1) => * Properties of pairs of bonds ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=66 +Id=70 Node(site_type:1<0) Id=0 Leaf False @@ -1135,13 +1135,13 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=68 - Node(site_type:0<0) +Id=65 + Node(site_type:2<0) Id=0 Leaf False - Id=67 - Node(site_type:0<2) + Id=4 + Node(site_type:2<2) Id=1 Leaf True @@ -1150,13 +1150,13 @@ Id=68 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=61 - Node(site_type:2<0) +Id=71 + Node(site_type:0<0) Id=0 Leaf False - Id=4 - Node(site_type:2<2) + Id=35 + Node(site_type:0<2) Id=1 Leaf True @@ -1165,12 +1165,12 @@ Id=61 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=68 +Id=71 Node(site_type:0<0) Id=0 Leaf False - Id=67 + Id=35 Node(site_type:0<2) Id=1 Leaf True @@ -1180,14 +1180,14 @@ Id=68 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=72 +Id=75 Node(site_type:1<0) Id=0 Leaf False - Id=71 + Id=74 Node(site_type:1<1) - Id=61 + Id=65 Node(site_type:2<0) Id=0 Leaf False @@ -1200,7 +1200,7 @@ Id=72 Id=0 Leaf False - Id=56 + Id=60 Node(site_type:1<2) Id=17 Node(site_type:2<0) @@ -1222,12 +1222,12 @@ EXTENSIONAL DESCRIPTION: ------------------------------------------------------------ * Export Views domain - non relational properties to JSon (internal constraints_list): ------------------------------------------------------------ -A()=> [ - A(t) - v A(t!A.t)] A()=> [ A(z~u?) v A(z~p?)] +A()=> [ + A(t) + v A(t!A.t)] A()=> [ A(z) v A(z!A.z)] diff --git a/models/test_suite/reachability_analysis/self_bond/output/LOG.ref b/models/test_suite/reachability_analysis/self_bond/output/LOG.ref index e44d1e5187..6387ce2f2c 100644 --- a/models/test_suite/reachability_analysis/self_bond/output/LOG.ref +++ b/models/test_suite/reachability_analysis/self_bond/output/LOG.ref @@ -921,12 +921,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for F(z!,t!) INTENSIONAL DESCRIPTION: -Id=23 +Id=25 Node(site_type:1<2) Id=0 Leaf False - Id=22 + Id=24 Node(site_type:1<3) Id=5 Node(site_type:2<0) @@ -1016,12 +1016,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for E(z!,t!) INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:1<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:1<1) Id=11 Node(site_type:2<1) @@ -1051,19 +1051,19 @@ EXTENSIONAL DESCRIPTION: Updating the views for D(z!,t!) INTENSIONAL DESCRIPTION: -Id=35 +Id=37 Node(site_type:1<1) Id=0 Leaf False - Id=34 + Id=36 Node(site_type:1<2) - Id=33 + Id=35 Node(site_type:2<2) Id=0 Leaf False - Id=32 + Id=34 Node(site_type:2<3) Id=1 Leaf True @@ -1081,12 +1081,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for D(z!,t!) INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:1<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:1<1) Id=11 Node(site_type:2<1) @@ -1111,19 +1111,19 @@ EXTENSIONAL DESCRIPTION: Updating the views for D(z!,t!) INTENSIONAL DESCRIPTION: -Id=41 +Id=43 Node(site_type:1<0) Id=0 Leaf False - Id=40 + Id=42 Node(site_type:1<1) - Id=33 + Id=35 Node(site_type:2<2) Id=0 Leaf False - Id=32 + Id=34 Node(site_type:2<3) Id=1 Leaf True @@ -1176,12 +1176,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for C(z!,t!) INTENSIONAL DESCRIPTION: -Id=31 +Id=33 Node(site_type:1<0) Id=0 Leaf False - Id=30 + Id=32 Node(site_type:1<1) Id=11 Node(site_type:2<1) @@ -1406,14 +1406,14 @@ Id=15 Leaf False agent_type:2:C:cv_id:0 -Id=29 +Id=31 Node(site_type:1<0) Id=0 Leaf False - Id=19 + Id=21 Node(site_type:1<2) - Id=18 + Id=20 Node(site_type:2<0) Id=0 Leaf False @@ -1430,19 +1430,19 @@ Id=29 Leaf False agent_type:3:D:cv_id:0 -Id=44 +Id=46 Node(site_type:1<0) Id=0 Leaf False - Id=43 + Id=45 Node(site_type:1<1) - Id=42 + Id=44 Node(site_type:2<0) Id=0 Leaf False - Id=32 + Id=34 Node(site_type:2<3) Id=1 Leaf True @@ -1450,14 +1450,14 @@ Id=44 Id=0 Leaf False - Id=34 + Id=36 Node(site_type:1<2) - Id=33 + Id=35 Node(site_type:2<2) Id=0 Leaf False - Id=32 + Id=34 Node(site_type:2<3) Id=1 Leaf True @@ -1469,14 +1469,14 @@ Id=44 Leaf False agent_type:4:E:cv_id:0 -Id=29 +Id=31 Node(site_type:1<0) Id=0 Leaf False - Id=19 + Id=21 Node(site_type:1<2) - Id=18 + Id=20 Node(site_type:2<0) Id=0 Leaf False @@ -1493,12 +1493,12 @@ Id=29 Leaf False agent_type:5:F:cv_id:0 -Id=26 +Id=28 Node(site_type:1<0) Id=0 Leaf False - Id=25 + Id=27 Node(site_type:1<1) Id=5 Node(site_type:2<0) @@ -1513,9 +1513,9 @@ Id=26 Id=0 Leaf False - Id=24 + Id=26 Node(site_type:1<2) - Id=18 + Id=20 Node(site_type:2<0) Id=0 Leaf False @@ -1528,7 +1528,7 @@ Id=26 Id=0 Leaf False - Id=22 + Id=24 Node(site_type:1<3) Id=5 Node(site_type:2<0) @@ -1551,7 +1551,7 @@ Id=26 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -1566,12 +1566,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -1581,7 +1581,7 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -1596,12 +1596,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -1611,7 +1611,7 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -1626,12 +1626,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -1641,12 +1641,12 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=54 +Id=56 Node(site_type:1<0) Id=0 Leaf False - Id=53 + Id=55 Node(site_type:1<3) Id=1 Leaf True @@ -1656,12 +1656,12 @@ Id=54 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -1671,7 +1671,7 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -1686,12 +1686,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -1701,7 +1701,7 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -1716,12 +1716,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=56 +Id=58 Node(site_type:0<0) Id=0 Leaf False - Id=55 + Id=57 Node(site_type:0<3) Id=1 Leaf True @@ -1747,12 +1747,12 @@ F() => [ F(z) v F(z!F.z) v F(z!F.t) ] * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=59 +Id=61 Node(site_type:0<0) Id=0 Leaf False - Id=58 + Id=60 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -1767,7 +1767,7 @@ Id=59 Id=0 Leaf False - Id=57 + Id=59 Node(site_type:0<2) Id=17 Node(site_type:1<1) @@ -1787,12 +1787,12 @@ Id=59 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=59 +Id=61 Node(site_type:0<0) Id=0 Leaf False - Id=58 + Id=60 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -1807,7 +1807,7 @@ Id=59 Id=0 Leaf False - Id=57 + Id=59 Node(site_type:0<2) Id=17 Node(site_type:1<1) @@ -1827,7 +1827,7 @@ Id=59 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -1842,12 +1842,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -1857,19 +1857,19 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=65 +Id=67 Node(site_type:0<0) Id=0 Leaf False - Id=64 + Id=66 Node(site_type:0<1) - Id=54 + Id=56 Node(site_type:1<0) Id=0 Leaf False - Id=53 + Id=55 Node(site_type:1<3) Id=1 Leaf True @@ -1877,14 +1877,14 @@ Id=65 Id=0 Leaf False - Id=63 + Id=65 Node(site_type:0<2) - Id=62 + Id=64 Node(site_type:1<2) Id=0 Leaf False - Id=53 + Id=55 Node(site_type:1<3) Id=1 Leaf True @@ -1897,7 +1897,7 @@ Id=65 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -1912,12 +1912,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -1927,12 +1927,12 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=71 +Id=73 Node(site_type:0<0) Id=0 Leaf False - Id=70 + Id=72 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -1947,9 +1947,9 @@ Id=71 Id=0 Leaf False - Id=69 + Id=71 Node(site_type:0<2) - Id=50 + Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -1962,7 +1962,7 @@ Id=71 Id=0 Leaf False - Id=68 + Id=70 Node(site_type:0<3) Id=3 Node(site_type:1<0) @@ -1997,7 +1997,7 @@ B(t!B.z,z!B.t) => [ B(t!2,z!1),B(t!1,z!2) v B(t!1,z!1) ] C(t!C.z,z!C.t) => C(t!2,z!1),C(t!1),C(z!2) E(t!E.t,z!E.z) => E(t!2,z!1),E(z!1),E(t!2) INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -2012,12 +2012,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -2027,7 +2027,7 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -2042,12 +2042,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -2057,7 +2057,7 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -2072,12 +2072,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -2087,12 +2087,12 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=54 +Id=56 Node(site_type:1<0) Id=0 Leaf False - Id=53 + Id=55 Node(site_type:1<3) Id=1 Leaf True @@ -2102,12 +2102,12 @@ Id=54 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -2117,7 +2117,7 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -2132,12 +2132,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -2147,7 +2147,7 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -2162,12 +2162,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=56 +Id=58 Node(site_type:0<0) Id=0 Leaf False - Id=55 + Id=57 Node(site_type:0<3) Id=1 Leaf True @@ -2177,12 +2177,12 @@ Id=56 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=59 +Id=61 Node(site_type:0<0) Id=0 Leaf False - Id=58 + Id=60 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -2197,7 +2197,7 @@ Id=59 Id=0 Leaf False - Id=57 + Id=59 Node(site_type:0<2) Id=17 Node(site_type:1<1) @@ -2217,12 +2217,12 @@ Id=59 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=59 +Id=61 Node(site_type:0<0) Id=0 Leaf False - Id=58 + Id=60 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -2237,7 +2237,7 @@ Id=59 Id=0 Leaf False - Id=57 + Id=59 Node(site_type:0<2) Id=17 Node(site_type:1<1) @@ -2257,7 +2257,7 @@ Id=59 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -2272,12 +2272,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -2287,19 +2287,19 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=65 +Id=67 Node(site_type:0<0) Id=0 Leaf False - Id=64 + Id=66 Node(site_type:0<1) - Id=54 + Id=56 Node(site_type:1<0) Id=0 Leaf False - Id=53 + Id=55 Node(site_type:1<3) Id=1 Leaf True @@ -2307,14 +2307,14 @@ Id=65 Id=0 Leaf False - Id=63 + Id=65 Node(site_type:0<2) - Id=62 + Id=64 Node(site_type:1<2) Id=0 Leaf False - Id=53 + Id=55 Node(site_type:1<3) Id=1 Leaf True @@ -2327,7 +2327,7 @@ Id=65 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=50 +Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -2342,12 +2342,12 @@ Id=50 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=52 +Id=54 Node(site_type:0<0) Id=0 Leaf False - Id=51 + Id=53 Node(site_type:0<2) Id=1 Leaf True @@ -2357,12 +2357,12 @@ Id=52 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=71 +Id=73 Node(site_type:0<0) Id=0 Leaf False - Id=70 + Id=72 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -2377,9 +2377,9 @@ Id=71 Id=0 Leaf False - Id=69 + Id=71 Node(site_type:0<2) - Id=50 + Id=52 Node(site_type:1<0) Id=0 Leaf False @@ -2392,7 +2392,7 @@ Id=71 Id=0 Leaf False - Id=68 + Id=70 Node(site_type:0<3) Id=3 Node(site_type:1<0) diff --git a/models/test_suite/reachability_analysis/side_effects/output/LOG.ref b/models/test_suite/reachability_analysis/side_effects/output/LOG.ref index 978cf0dd17..4e8c3bee1a 100644 --- a/models/test_suite/reachability_analysis/side_effects/output/LOG.ref +++ b/models/test_suite/reachability_analysis/side_effects/output/LOG.ref @@ -1358,7 +1358,7 @@ Id=52 Id=51 Node(site_type:1<2) - Id=30 + Id=32 Node(site_type:2<0) Id=0 Leaf False @@ -1375,12 +1375,12 @@ Id=52 Leaf False agent_type:1:B:cv_id:0 -Id=29 +Id=31 Node(site_type:1<0) Id=0 Leaf False - Id=28 + Id=30 Node(site_type:1<1) Id=5 Node(site_type:2<0) @@ -1395,7 +1395,7 @@ Id=29 Id=0 Leaf False - Id=27 + Id=29 Node(site_type:1<2) Id=22 Node(site_type:2<0) @@ -1453,12 +1453,12 @@ Id=26 Leaf False agent_type:3:D:cv_id:0 -Id=29 +Id=31 Node(site_type:1<0) Id=0 Leaf False - Id=28 + Id=30 Node(site_type:1<1) Id=5 Node(site_type:2<0) @@ -1473,7 +1473,7 @@ Id=29 Id=0 Leaf False - Id=27 + Id=29 Node(site_type:1<2) Id=22 Node(site_type:2<0) @@ -1492,12 +1492,12 @@ Id=29 Leaf False agent_type:4:E:cv_id:0 -Id=29 +Id=31 Node(site_type:1<0) Id=0 Leaf False - Id=28 + Id=30 Node(site_type:1<1) Id=5 Node(site_type:2<0) @@ -1512,7 +1512,7 @@ Id=29 Id=0 Leaf False - Id=27 + Id=29 Node(site_type:1<2) Id=22 Node(site_type:2<0) diff --git a/models/test_suite/reachability_analysis/site_accross_bonds_domain/output/LOG.ref b/models/test_suite/reachability_analysis/site_accross_bonds_domain/output/LOG.ref index 379d92afd3..82bd69a465 100644 --- a/models/test_suite/reachability_analysis/site_accross_bonds_domain/output/LOG.ref +++ b/models/test_suite/reachability_analysis/site_accross_bonds_domain/output/LOG.ref @@ -729,12 +729,12 @@ EXTENSIONAL DESCRIPTION: Updating the views for B(z~,z!,t~) INTENSIONAL DESCRIPTION: -Id=70 +Id=72 Node(site_type:1<1) Id=0 Leaf False - Id=69 + Id=71 Node(site_type:1<2) Id=63 Node(site_type:2<0) @@ -844,12 +844,12 @@ Id=55 Leaf False agent_type:1:B:cv_id:0 -Id=74 +Id=76 Node(site_type:1<0) Id=0 Leaf False - Id=73 + Id=75 Node(site_type:1<1) Id=63 Node(site_type:2<0) @@ -874,9 +874,9 @@ Id=74 Id=0 Leaf False - Id=72 + Id=74 Node(site_type:1<2) - Id=71 + Id=73 Node(site_type:2<0) Id=0 Leaf False @@ -922,7 +922,7 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=81 Node(site_type:0<0) Id=0 Leaf False @@ -937,13 +937,13 @@ Id=75 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=66 - Node(site_type:1<0) +Id=39 + Node(site_type:2<0) Id=0 Leaf False - Id=12 - Node(site_type:1<2) + Id=20 + Node(site_type:2<2) Id=1 Leaf True @@ -952,13 +952,13 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=39 - Node(site_type:2<0) +Id=66 + Node(site_type:1<0) Id=0 Leaf False - Id=20 - Node(site_type:2<2) + Id=12 + Node(site_type:1<2) Id=1 Leaf True @@ -967,7 +967,7 @@ Id=39 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=81 Node(site_type:0<0) Id=0 Leaf False @@ -983,8 +983,8 @@ Id=75 EXTENSIONAL DESCRIPTION: A() => [ A(t~u) v A(t~p) ] A() => [ A(z) v A(z!B.z) ] -B() => [ B(z) v B(z!A.z) ] B() => [ B(t~u) v B(t~p) ] +B() => [ B(z) v B(z!A.z) ] B() => [ B(z~u?) v B(z~p?) ] ------------------------------------------------------------ @@ -1006,7 +1006,7 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=81 Node(site_type:0<0) Id=0 Leaf False @@ -1036,12 +1036,12 @@ Id=39 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=81 +Id=87 Node(site_type:0<0) Id=0 Leaf False - Id=80 + Id=86 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -1056,7 +1056,7 @@ Id=81 Id=0 Leaf False - Id=79 + Id=85 Node(site_type:0<2) Id=66 Node(site_type:1<0) @@ -1083,6 +1083,7 @@ A(z!1),B(z!1) => [ A(t~p,z!1),B(t~p,z!1) v A(t~u,z!1),B(t~u,z!1) + v A(t~u,z!1),B(t~p,z!1) ] ------------------------------------------------------------ * Properties of pairs of bonds @@ -1103,7 +1104,7 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=81 Node(site_type:0<0) Id=0 Leaf False @@ -1118,13 +1119,13 @@ Id=75 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=66 - Node(site_type:1<0) +Id=39 + Node(site_type:2<0) Id=0 Leaf False - Id=12 - Node(site_type:1<2) + Id=20 + Node(site_type:2<2) Id=1 Leaf True @@ -1133,13 +1134,13 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=39 - Node(site_type:2<0) +Id=66 + Node(site_type:1<0) Id=0 Leaf False - Id=20 - Node(site_type:2<2) + Id=12 + Node(site_type:1<2) Id=1 Leaf True @@ -1148,7 +1149,7 @@ Id=39 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=81 Node(site_type:0<0) Id=0 Leaf False @@ -1178,7 +1179,7 @@ Id=66 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=81 Node(site_type:0<0) Id=0 Leaf False @@ -1208,12 +1209,12 @@ Id=39 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=81 +Id=87 Node(site_type:0<0) Id=0 Leaf False - Id=80 + Id=86 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -1228,7 +1229,7 @@ Id=81 Id=0 Leaf False - Id=79 + Id=85 Node(site_type:0<2) Id=66 Node(site_type:1<0) @@ -1253,12 +1254,12 @@ EXTENSIONAL DESCRIPTION: B()=> [ B(z~u?) v B(z~p?)] -B()=> [ - B(t~u) - v B(t~p)] B()=> [ B(z) v B(z!A.z)] +B()=> [ + B(t~u) + v B(t~p)] A()=> [ A(z) v A(z!B.z)] @@ -1276,7 +1277,8 @@ B(z!A.z)=> [B(z~p!A.z)] ------------------------------------------------------------ A(z!1),B(z!1)=> [ A(t~p,z!1),B(t~p,z!1) - v A(t~u,z!1),B(t~u,z!1)] + v A(t~u,z!1),B(t~u,z!1) + v A(t~u,z!1),B(t~p,z!1)] ------------------------------------------------------------ * Export Parallel bonds to JSon (internal constraints_list): diff --git a/models/test_suite/reachability_analysis/site_accross_bonds_domain_2/output/LOG.ref b/models/test_suite/reachability_analysis/site_accross_bonds_domain_2/output/LOG.ref index 665f9d71e8..69b046e1cd 100644 --- a/models/test_suite/reachability_analysis/site_accross_bonds_domain_2/output/LOG.ref +++ b/models/test_suite/reachability_analysis/site_accross_bonds_domain_2/output/LOG.ref @@ -768,12 +768,12 @@ Id=62 Leaf False agent_type:1:B:cv_id:0 -Id=74 +Id=80 Node(site_type:1<0) Id=0 Leaf False - Id=73 + Id=79 Node(site_type:1<1) Id=13 Node(site_type:2<0) @@ -798,14 +798,14 @@ Id=74 Id=0 Leaf False - Id=72 + Id=78 Node(site_type:1<2) - Id=71 + Id=77 Node(site_type:2<0) Id=0 Leaf False - Id=70 + Id=76 Node(site_type:2<1) Id=11 Node(site_type:3<0) @@ -846,7 +846,7 @@ Id=74 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=77 +Id=87 Node(site_type:1<0) Id=0 Leaf False @@ -861,7 +861,7 @@ Id=77 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=76 +Id=86 Node(site_type:0<0) Id=0 Leaf False @@ -876,7 +876,7 @@ Id=76 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=85 Node(site_type:1<0) Id=0 Leaf False @@ -891,13 +891,13 @@ Id=75 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=76 - Node(site_type:0<0) +Id=37 + Node(site_type:2<0) Id=0 Leaf False - Id=53 - Node(site_type:0<2) + Id=18 + Node(site_type:2<2) Id=1 Leaf True @@ -906,13 +906,13 @@ Id=76 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=37 - Node(site_type:2<0) +Id=86 + Node(site_type:0<0) Id=0 Leaf False - Id=18 - Node(site_type:2<2) + Id=53 + Node(site_type:0<2) Id=1 Leaf True @@ -923,19 +923,19 @@ EXTENSIONAL DESCRIPTION: A() => [ A(t~u) v A(t~p) v A(t~q) ] A() => [ A(z) v A(z!B.z) ] B() => [ B(z) v B(z!A.z) ] -B() => [ B(z~u?) v B(z~p?) ] B() => [ B(t~u) v B(t~p) ] +B() => [ B(z~u?) v B(z~p?) ] ------------------------------------------------------------ * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=81 +Id=91 Node(site_type:0<0) Id=0 Leaf False - Id=80 + Id=90 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -950,9 +950,9 @@ Id=81 Id=0 Leaf False - Id=79 + Id=89 Node(site_type:0<2) - Id=77 + Id=87 Node(site_type:1<0) Id=0 Leaf False @@ -970,12 +970,12 @@ Id=81 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=97 +Id=107 Node(site_type:0<0) Id=0 Leaf False - Id=96 + Id=106 Node(site_type:0<1) Id=7 Node(site_type:1<0) @@ -1000,7 +1000,7 @@ Id=97 Id=0 Leaf False - Id=95 + Id=105 Node(site_type:0<2) Id=40 Node(site_type:1<0) @@ -1052,14 +1052,15 @@ B(z) => B(t~u,z) ------------------------------------------------------------ A(z!1),B(z!1) => [ - A(t~p,z!1),B(t~p,z!1) + A(t~q,z!1),B(t~p,z!1) + v A(t~p,z!1),B(t~p,z!1) v A(t~u,z!1),B(t~u,z!1) ] ------------------------------------------------------------ * Properties of pairs of bonds ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=77 +Id=87 Node(site_type:1<0) Id=0 Leaf False @@ -1074,7 +1075,7 @@ Id=77 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=76 +Id=86 Node(site_type:0<0) Id=0 Leaf False @@ -1089,7 +1090,7 @@ Id=76 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=75 +Id=85 Node(site_type:1<0) Id=0 Leaf False @@ -1104,13 +1105,13 @@ Id=75 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=76 - Node(site_type:0<0) +Id=37 + Node(site_type:2<0) Id=0 Leaf False - Id=53 - Node(site_type:0<2) + Id=18 + Node(site_type:2<2) Id=1 Leaf True @@ -1119,13 +1120,13 @@ Id=76 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=37 - Node(site_type:2<0) +Id=86 + Node(site_type:0<0) Id=0 Leaf False - Id=18 - Node(site_type:2<2) + Id=53 + Node(site_type:0<2) Id=1 Leaf True @@ -1134,12 +1135,12 @@ Id=37 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=81 +Id=91 Node(site_type:0<0) Id=0 Leaf False - Id=80 + Id=90 Node(site_type:0<1) Id=3 Node(site_type:1<0) @@ -1154,9 +1155,9 @@ Id=81 Id=0 Leaf False - Id=79 + Id=89 Node(site_type:0<2) - Id=77 + Id=87 Node(site_type:1<0) Id=0 Leaf False @@ -1174,12 +1175,12 @@ Id=81 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=97 +Id=107 Node(site_type:0<0) Id=0 Leaf False - Id=96 + Id=106 Node(site_type:0<1) Id=7 Node(site_type:1<0) @@ -1204,7 +1205,7 @@ Id=97 Id=0 Leaf False - Id=95 + Id=105 Node(site_type:0<2) Id=40 Node(site_type:1<0) @@ -1251,12 +1252,12 @@ EXTENSIONAL DESCRIPTION: ------------------------------------------------------------ * Export Views domain - non relational properties to JSon (internal constraints_list): ------------------------------------------------------------ -B()=> [ - B(t~u) - v B(t~p)] B()=> [ B(z~u?) v B(z~p?)] +B()=> [ + B(t~u) + v B(t~p)] B()=> [ B(z) v B(z!A.z)] @@ -1279,7 +1280,8 @@ A(z)=> [A(t~u,z)] * Export Connected agents to JSon (internal constraints_list): ------------------------------------------------------------ A(z!1),B(z!1)=> [ - A(t~p,z!1),B(t~p,z!1) + A(t~q,z!1),B(t~p,z!1) + v A(t~p,z!1),B(t~p,z!1) v A(t~u,z!1),B(t~u,z!1)] ------------------------------------------------------------ diff --git a/models/test_suite/symmetries/sym2/output/LOG.ref b/models/test_suite/symmetries/sym2/output/LOG.ref index 2a7b2cd34d..4cb84e9da9 100644 --- a/models/test_suite/symmetries/sym2/output/LOG.ref +++ b/models/test_suite/symmetries/sym2/output/LOG.ref @@ -844,14 +844,14 @@ every agent may occur in the model * Fixpoint iteration : ------------------------------------------------------------ agent_type:0:A:cv_id:0 -Id=32 +Id=38 Node(site_type:1<0) Id=0 Leaf False - Id=31 + Id=37 Node(site_type:1<1) - Id=30 + Id=36 Node(site_type:2<0) Id=0 Leaf False @@ -887,7 +887,7 @@ Id=32 * Non relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=33 +Id=39 Node(site_type:1<0) Id=0 Leaf False @@ -902,7 +902,7 @@ Id=33 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=35 +Id=40 Node(site_type:0<0) Id=0 Leaf False @@ -923,14 +923,14 @@ A() => [ A(x) v A(x!A.x) v A(x!A.y) ] * Relational properties: ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=40 +Id=45 Node(site_type:0<0) Id=0 Leaf False - Id=39 + Id=44 Node(site_type:0<1) - Id=33 + Id=39 Node(site_type:1<0) Id=0 Leaf False @@ -943,7 +943,7 @@ Id=40 Id=0 Leaf False - Id=38 + Id=43 Node(site_type:0<3) Id=3 Node(site_type:1<0) @@ -971,7 +971,7 @@ A(x!A.x) => A(x!A.x,y) * Properties of pairs of bonds ------------------------------------------------------------ INTENSIONAL DESCRIPTION: -Id=33 +Id=39 Node(site_type:1<0) Id=0 Leaf False @@ -986,7 +986,7 @@ Id=33 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=35 +Id=40 Node(site_type:0<0) Id=0 Leaf False @@ -1001,14 +1001,14 @@ Id=35 EXTENSIONAL DESCRIPTION: INTENSIONAL DESCRIPTION: -Id=40 +Id=45 Node(site_type:0<0) Id=0 Leaf False - Id=39 + Id=44 Node(site_type:0<1) - Id=33 + Id=39 Node(site_type:1<0) Id=0 Leaf False @@ -1021,7 +1021,7 @@ Id=40 Id=0 Leaf False - Id=38 + Id=43 Node(site_type:0<3) Id=3 Node(site_type:1<0)