Commit a4e26a9e authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

Proper rule-deletion from counter-ex (only! when available)

parent 7a817565
......@@ -42,8 +42,9 @@ revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
item([kind: option, item: option(nusmv_initial_states: Init)]),
item([kind: option, item: option(boolean_semantics: Bool)]),
check_ctl_impl(U, Init, silent, Bool, Result),
(
check_ctl_impl(U, Init, silent, Bool, true)
Result = true
->
print_message(informational, step('U'))
;
......@@ -65,8 +66,9 @@ revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
revise_model([], [], [A | ACTL], Et, Ut, At) :-
item([kind: option, item: option(nusmv_initial_states: Init)]),
item([kind: option, item: option(boolean_semantics: Bool)]),
check_ctl_impl(A, Init, silent, Bool, Result),
(
check_ctl_impl(A, Init, silent, Bool, true)
Result = true
->
print_message(informational, step('A'))
;
......@@ -223,10 +225,8 @@ find_and_delete_rules :-
(
nusmv:trace(_)
->
write('trace!'),nl,
delete_rules_from_trace
;
write('notrace :('),nl,
delete_rules
).
......@@ -235,7 +235,6 @@ delete_rules_from_trace :-
enumerate_all_molecules(Molecules),
findall(State, nusmv:trace(State), States),
rules_from_trace(States, Molecules, Rules),
write(rules(Rules)),nl,
% We cut a single state-transition, if necessary by removing several rules
member(ToBeDeleted, Rules),
maplist(del_reaction_backtracking, ToBeDeleted).
......
......@@ -45,32 +45,30 @@ test(
test(
'revise_model rule deletion for ACTL',
'revise_model rule deletion for ACTL, Miguel example',
[
setup(clear_model),
all(Reactions = [[], [b => c]])
all(Reactions = [['_' =[a]=> b]])
]
) :-
command(present(a)),
command(absent(b)),
command(add_reaction(a => b)),
command(add_reaction(b => c)),
revise_model('AG'(a)),
command(add_reaction(a => a + b)),
command(add_reaction(a + b => b)),
revise_model(not(a) \/ 'AX'(a /\ b)),
findall(Item, item([kind: reaction, item: Item]), Reactions).
test(
'revise_model rule deletion for ACTL, deleting from NuSMV counter-example',
'revise_model rule deletion (from counter-example) for ACTL',
[
setup(clear_model),
all(Reactions = [['_' =[a]=> b]])
all(Reactions = [[], [b => c]])
]
) :-
command(present(a)),
command(present(b)),
command(add_reaction(a => a + b)),
command(add_reaction(a + b => b)),
revise_model('AX'(a /\ b)),
command(absent(b)),
command(add_reaction(a => b)),
command(add_reaction(b => c)),
revise_model('AG'(a)),
findall(Item, item([kind: reaction, item: Item]), Reactions).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment