Skip to content

Commit 32fa0e1

Browse files
feretferet
committed
bugfix, issue #393: solve the soundness issue, at the cost of a loss of accuracy in the case of asymetric binding, a collaboration between site-across-bonds domain and parallel bond domain is required
1 parent 8336eb1 commit 32fa0e1

File tree

27 files changed

+971
-903
lines changed

27 files changed

+971
-903
lines changed

‎KaSa_rep/reachability_analysis/site_across_bonds_domain.ml‎

Lines changed: 159 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
* Jérôme Feret & Ly Kim Quyen, project Antique, INRIA Paris
55
*
66
* Creation: 2016, the 31th of March
7-
* Last modification: Time-stamp: <Apr 08 2017>
7+
* Last modification: Time-stamp: <Apr 27 2017>
88
*
99
* Abstract domain to record relations between pair of sites in connected agents.
1010
*
@@ -972,8 +972,31 @@ struct
972972
(*APPLY RULE*)
973973
(***************************************************************************)
974974

975+
let check_association_list
976+
parameters error bdu_false
977+
pair
978+
check
979+
dynamic
980+
=
981+
let store_result = get_value dynamic in
982+
let handler = get_mvbdu_handler dynamic in
983+
let error, handler, mvbdu =
984+
Ckappa_sig.Views_bdu.mvbdu_of_association_list
985+
parameters handler error check
986+
in
987+
let error, handler, bool =
988+
Site_across_bonds_domain_type.check
989+
parameters error bdu_false handler
990+
pair
991+
mvbdu
992+
store_result
993+
in
994+
let dynamic = set_mvbdu_handler handler dynamic in
995+
error, dynamic, bool
975996
(*there is an action binding in the domain of a rule*)
976997

998+
999+
9771000
let build_mvbdu_association_list parameters error bdu_false
9781001
kappa_handler dump_title bool modified_sites pair pair_list dynamic =
9791002
let store_result = get_value dynamic in
@@ -1205,19 +1228,53 @@ struct
12051228
let dynamic = set_global_dynamic_information global_dynamic dynamic in
12061229
error, dynamic, precondition, state_list
12071230

1231+
1232+
12081233
let get_state_of_site_in_precondition_2
1209-
error static dynamic rule agent_id
1210-
(site_type_x, agent_type_y, site_type_y)
1211-
site_type'_y
1234+
error static dynamic rule
1235+
agent_id agent_type site
12121236
precondition =
1213-
let defined_in = Communication.LHS rule in
1214-
get_state_of_site_in_pre_post_condition_2
1215-
error static dynamic
1216-
agent_id
1217-
(site_type_x, agent_type_y, site_type_y)
1218-
site_type'_y
1219-
defined_in
1220-
precondition
1237+
1238+
let path =
1239+
{
1240+
Communication.defined_in = Communication.LHS rule;
1241+
path =
1242+
{
1243+
Communication.agent_id = agent_id;
1244+
Communication.relative_address = [];
1245+
Communication.site = site}
1246+
}
1247+
in
1248+
let error, global_dynamic, precondition, state_list_lattice =
1249+
Communication.get_state_of_site
1250+
error
1251+
precondition
1252+
(get_global_static_information static)
1253+
(get_global_dynamic_information dynamic)
1254+
path
1255+
in
1256+
let error, state_list =
1257+
match state_list_lattice with
1258+
| Usual_domains.Val l -> error, l
1259+
| Usual_domains.Undefined -> error, []
1260+
| Usual_domains.Any ->
1261+
let parameter = get_parameter static in
1262+
let error, () =
1263+
if Remanent_parameters.get_view_analysis parameter
1264+
then
1265+
Exception.warn
1266+
(get_parameter static) error __POS__ Exit ()
1267+
else
1268+
error, ()
1269+
in
1270+
let kappa_handler = get_kappa_handler static in
1271+
Handler.state_list
1272+
parameter kappa_handler error agent_type site
1273+
in
1274+
let dynamic = set_global_dynamic_information global_dynamic dynamic in
1275+
error, dynamic, precondition, state_list
1276+
1277+
12211278

12221279
let get_state_of_site_in_postcondition_2
12231280
error static dynamic rule agent_id
@@ -1232,6 +1289,7 @@ struct
12321289
defined_in
12331290
precondition
12341291

1292+
12351293
type pos = Fst | Snd
12361294

12371295
let get_partition_modified pos static =
@@ -1260,6 +1318,8 @@ struct
12601318
(site_type_y, agent_type_x, site_type_x) site_type'_x
12611319
precondition
12621320

1321+
1322+
12631323
let get_potential_tuple_pair parameters error (agent, site) empty_map map =
12641324
let error, result =
12651325
match
@@ -1341,13 +1401,47 @@ struct
13411401
| Snd -> site_type'_x))
13421402
__POS__ Exit
13431403
in
1404+
let error', dynamic, precondition, state_list_other =
1405+
let error, agent =
1406+
match
1407+
Ckappa_sig.Agent_id_quick_nearly_Inf_Int_storage_Imperatif.get
1408+
parameters
1409+
error
1410+
agent_id_mod
1411+
rule.Cckappa_sig.e_rule_c_rule.Cckappa_sig.rule_lhs.Cckappa_sig.views
1412+
with
1413+
| error, None ->
1414+
Exception.warn parameters error __POS__ Exit Cckappa_sig.Ghost
1415+
| error, Some a -> error, a
1416+
in
1417+
match agent with
1418+
| Cckappa_sig.Ghost
1419+
| Cckappa_sig.Unknown_agent _
1420+
| Cckappa_sig.Dead_agent _ ->
1421+
error, dynamic, precondition, []
1422+
| Cckappa_sig.Agent agent ->
1423+
get_state_of_site_in_precondition_2
1424+
error static dynamic
1425+
(rule_id, rule)
1426+
agent_id_mod agent_type_mod site_type_mod
1427+
precondition
1428+
in
1429+
let error =
1430+
Exception.check_point
1431+
Exception.warn
1432+
parameters error error'
1433+
~message:(context rule_id agent_id_mod site_type_mod)
1434+
__POS__ Exit
1435+
in
13441436
(*-----------------------------------------------------------*)
13451437
let error, bool, dynamic, precondition, modified_sites =
1346-
match state'_list_other with
1347-
| [] | _::_::_ ->
1348-
(* we know for sure that the site has not been modified *)
1349-
error, bool, dynamic, precondition, modified_sites
1350-
| [_] ->
1438+
let not_modified =
1439+
match state'_list_other with
1440+
| [] | _::_::_ -> true
1441+
(* we know for sure that the site has not been modified *)
1442+
1443+
| [_] -> false
1444+
in
13511445
List.fold_left
13521446
(fun (error, bool, dynamic, precondition, modified_sites)
13531447
state'_other ->
@@ -1364,17 +1458,58 @@ struct
13641458
(agent_type_x, site_type_x, site_type'_x,state_x),
13651459
(agent_type_y, site_type_y, site_type'_y,state_y)
13661460
in
1367-
let error, bool, dynamic, modified_sites =
1368-
build_mvbdu_association_list
1461+
let check =
1462+
match state_list_other,pos
1463+
with
1464+
([] | _::_::_),_ -> []
1465+
| [a],Fst ->
1466+
[Ckappa_sig.fst_site, a]
1467+
| [a],Snd ->
1468+
[Ckappa_sig.snd_site, a]
1469+
in
1470+
let check =
1471+
if not_modified
1472+
then
1473+
match pos with
1474+
| Fst ->
1475+
(* to do: add info about the other site *)
1476+
(* if the bond between site_type_x and site_type_y
1477+
has not been created by the rule *)
1478+
(* this is the state before the modification *)
1479+
(* otherwise, nothing to check *)
1480+
(Ckappa_sig.snd_site, state'_other)::check
1481+
| Snd ->
1482+
(* to do: add info about the other site *)
1483+
(* if the bond between site_type_x and site_type_y
1484+
has not been created by the rule *)
1485+
(* this is the state before the modification *)
1486+
(* this is the state before the modification *)
1487+
(Ckappa_sig.fst_site, state'_other)::check
1488+
else
1489+
check
1490+
in
1491+
let error, dynamic, unmodified_sites_ok =
1492+
check_association_list
13691493
parameters error bdu_false
1370-
kappa_handler dump_title
1371-
bool
1372-
modified_sites
13731494
pair
1374-
pair_list
1495+
check
13751496
dynamic
13761497
in
1377-
error, bool, dynamic, precondition, modified_sites
1498+
if unmodified_sites_ok
1499+
then
1500+
let error, bool, dynamic, modified_sites =
1501+
build_mvbdu_association_list
1502+
parameters error bdu_false
1503+
kappa_handler dump_title
1504+
bool
1505+
modified_sites
1506+
pair
1507+
pair_list
1508+
dynamic
1509+
in
1510+
error, bool, dynamic, precondition, modified_sites
1511+
else
1512+
error, bool, dynamic, precondition, modified_sites
13781513
)
13791514
(error, bool, dynamic, precondition, modified_sites)
13801515
state'_list_other

‎KaSa_rep/reachability_analysis/site_across_bonds_domain_type.ml‎

Lines changed: 20 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
* Jérôme Feret & Ly Kim Quyen, project Antique, INRIA Paris-Rocquencourt
55
*
66
* Creation: 2016, the 31th of March
7-
* Last modification: Time-stamp: <Apr 08 2017>
7+
* Last modification: Time-stamp: <Apr 27 2017>
88
*
99
* Abstract domain to record relations between pair of sites in connected agents.
1010
*
@@ -504,6 +504,25 @@ let add_sites_from_tuples parameters error tuple modified_sites =
504504
(error, modified_sites)
505505
[agent,site1;agent,site2;agent',site1';agent',site2']
506506

507+
let check
508+
parameters error bdu_false handler
509+
pair
510+
mvbdu
511+
store_result
512+
=
513+
let error, bdu_old =
514+
get_mvbdu_from_tuple_pair parameters error pair bdu_false store_result
515+
in
516+
let error, handler, new_bdu =
517+
Ckappa_sig.Views_bdu.mvbdu_and
518+
parameters handler error bdu_old mvbdu
519+
in
520+
if Ckappa_sig.Views_bdu.equal new_bdu bdu_false
521+
then
522+
error, handler, false
523+
else
524+
error, handler, true
525+
507526
let add_link_and_check parameter error bdu_false handler
508527
kappa_handler bool dump_title x mvbdu modified_sites store_result =
509528
let error, bdu_old =

‎models/test_suite/CMSB_paper/dimer/output/LOG.ref‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -42,11 +42,6 @@ R(c!1),R(c!1) =>
4242
v R(c!1,cr),R(c!1,cr)
4343
v R(c!1,cr),R(c!1,cr!R.n)
4444
]
45-
R(c!1),R(c!1) =>
46-
[
47-
R(c!1,cr!R.n),R(c!1,n!R.cr)
48-
v R(c!1,cr),R(c!1,n)
49-
]
5045
R(c!1),R(c!1) =>
5146
[
5247
R(c!1,n!R.cr),R(c!1,n)

‎models/test_suite/CMSB_paper/dimer_all_domains/output/LOG.ref‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -42,11 +42,6 @@ R(c!1),R(c!1) =>
4242
v R(c!1,cr),R(c!1,cr)
4343
v R(c!1,cr),R(c!1,cr!R.n)
4444
]
45-
R(c!1),R(c!1) =>
46-
[
47-
R(c!1,cr!R.n),R(c!1,n!R.cr)
48-
v R(c!1,cr),R(c!1,n)
49-
]
5045
R(c!1),R(c!1) =>
5146
[
5247
R(c!1,n!R.cr),R(c!1,n)

‎models/test_suite/CMSB_paper/dimer_cm_views_site_across_bonds/output/LOG.ref‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -42,11 +42,6 @@ R(c!1),R(c!1) =>
4242
v R(c!1,cr),R(c!1,cr)
4343
v R(c!1,cr),R(c!1,cr!R.n)
4444
]
45-
R(c!1),R(c!1) =>
46-
[
47-
R(c!1,cr!R.n),R(c!1,n!R.cr)
48-
v R(c!1,cr),R(c!1,n)
49-
]
5045
R(c!1),R(c!1) =>
5146
[
5247
R(c!1,n!R.cr),R(c!1,n)

‎models/test_suite/CMSB_paper/dimer_views_site_across_bonds/output/LOG.ref‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -42,11 +42,6 @@ R(c!1),R(c!1) =>
4242
v R(c!1,cr),R(c!1,cr)
4343
v R(c!1,cr),R(c!1,cr!R.n)
4444
]
45-
R(c!1),R(c!1) =>
46-
[
47-
R(c!1,cr!R.n),R(c!1,n!R.cr)
48-
v R(c!1,cr),R(c!1,n)
49-
]
5045
R(c!1),R(c!1) =>
5146
[
5247
R(c!1,n!R.cr),R(c!1,n)

‎models/test_suite/CMSB_paper/dimer_views_site_across_bonds_double_bonds/output/LOG.ref‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -42,11 +42,6 @@ R(c!1),R(c!1) =>
4242
v R(c!1,cr),R(c!1,cr)
4343
v R(c!1,cr),R(c!1,cr!R.n)
4444
]
45-
R(c!1),R(c!1) =>
46-
[
47-
R(c!1,cr!R.n),R(c!1,n!R.cr)
48-
v R(c!1,cr),R(c!1,n)
49-
]
5045
R(c!1),R(c!1) =>
5146
[
5247
R(c!1,n!R.cr),R(c!1,n)

‎models/test_suite/CMSB_paper/sos/output/LOG.ref‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,9 @@ every agent may occur in the model
1818
EGF() => [ EGF(r) v EGF(r!EGFR.L) ]
1919
EGFR() => [ EGFR(Y1092~u?) v EGFR(Y1092~p?) ]
2020
EGFR() => [ EGFR(Y1172~u?) v EGFR(Y1172~p?) ]
21-
EGFR() => EGFR(Y1016~u)
2221
EGFR() => [ EGFR(L) v EGFR(L!EGF.r) ]
2322
EGFR() => [ EGFR(CR) v EGFR(CR!EGFR.CR) ]
23+
EGFR() => EGFR(Y1016~u)
2424
EGFR() => [ EGFR(N) v EGFR(N!EGFR.C) ]
2525
EGFR() => [ EGFR(C) v EGFR(C!EGFR.N) ]
2626
EGFR() => [ EGFR(Y1172) v EGFR(Y1172!Shc.PTB) ]
@@ -29,8 +29,8 @@ SoS() => [ SoS(PR) v SoS(PR!Grb2.SH3n) ]
2929
SoS() => SoS(S~u)
3030
Shc() => Shc(PTB~u?)
3131
Shc() => [ Shc(Y) v Shc(Y!Grb2.SH2) ]
32-
Shc() => [ Shc(Y~u?) v Shc(Y~p?) ]
3332
Shc() => [ Shc(PTB) v Shc(PTB!EGFR.Y1172) ]
33+
Shc() => [ Shc(Y~u?) v Shc(Y~p?) ]
3434
Grb2() => [ Grb2(SH2) v Grb2(SH2!Shc.Y) v Grb2(SH2!EGFR.Y1092) ]
3535
Grb2() => [ Grb2(SH3n) v Grb2(SH3n!SoS.PR) ]
3636
Grb2() => Grb2(SH2~u?)

0 commit comments

Comments
 (0)