Commit a7a8c5f5 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

cleanup and refactor, paving the way for rule deletion

parent c6791a7e
......@@ -519,11 +519,11 @@ check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :-
open('nusmv.cmd', write, Stream),
write(Stream, 'set input_file nusmv.smv\ngo\n'),
(
NusmvCX == 'yes'
NusmvCX == 'no'
->
write(Stream, 'set default_trace_plugin 2\nset counter_examples 1\n')
;
write(Stream, 'set counter_examples 0\n')
;
write(Stream, 'set default_trace_plugin 2\nset counter_examples 1\n')
),
format(Stream, 'check_ctlspec -p "~a"\nquit\n', [NusmvQuery]),
close(Stream),
......@@ -617,11 +617,11 @@ parse_nusmv_out(Out, NusmvCX, Result) :-
Result = 'error'
),
(
NusmvCX == 'yes'
NusmvCX == 'no'
->
parse_nusmv_out_trace(Out)
;
true
;
parse_nusmv_out_trace(Out)
),
close(Out)
;
......
......@@ -23,74 +23,60 @@ revise_model(Query) :-
% Everything copied as much as possible from CCFS05tcsb
revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
revise_model([E | ECTL], 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, no, Bool, true)
check_ctl_impl(E, Init, no, Bool, true)
->
print_message(informational, step('U')),
% step U
revise_model([], UCTL, ACTL, Et, [U | Ut], At)
print_message(informational, step('E'))
;
print_message(informational, step('U''')),
% step U'
% try to find some rule from the pattern
find_rule(R),
print_message(informational, trying(R)),
add_reaction_backtracking(R),
print_message(informational, step('E''')),
find_and_add_rule,
% FIXME check Et too since self-loops can be broken by adding a reaction
append([U | Ut], At, AllSpec),
join_op('/\\', AllSpec, Spec),
print_message(informational, checking(Spec)),
check_ctl_impl(Spec, Init, no, Bool, true)
->
revise_model([], UCTL, ACTL, Et, [U | Ut], At)
;
print_message(informational, step('U''''')),
% step U''
% try to find some rule from the trace and delete it
fail
).
append([E | Ut], At, AllSpec),
recheck_spec(AllSpec, Init, Bool)
),
revise_model(ECTL, UCTL, ACTL, [E | Et], Ut, At).
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(E, Init, no, Bool, true)
check_ctl_impl(U, Init, silent, Bool, true)
->
print_message(informational, step('E')),
% step E
revise_model(ECTL, UCTL, ACTL, [E | Et], Ut, At)
print_message(informational, step('U'))
;
print_message(informational, step('E''')),
% step E'
% try to find some rule from the pattern
find_rule(R),
add_reaction_backtracking(R),
% FIXME check Et too since self-loops can be broken by adding a reaction
append([E | Ut], At, AllSpec),
join_op('/\\', AllSpec, Spec),
print_message(informational, checking(Spec)),
check_ctl_impl(Spec, Init, no, Bool, true),
revise_model(ECTL, UCTL, ACTL, [E | Et], Ut, At)
).
(
print_message(informational, step('U''')),
find_and_add_rule,
% FIXME check Et too since self-loops can be broken by adding a reaction
append([U | Ut], At, AllSpec)
;
print_message(informational, step('U''''')),
find_and_delete_rules,
% FIXME check At too since self-loops can be added by removing a reaction
append([U | Ut], Et, AllSpec)
),
recheck_spec(AllSpec, Init, Bool)
),
revise_model([], UCTL, ACTL, Et, [U | 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, no, Bool, true)
check_ctl_impl(A, Init, silent, Bool, true)
->
print_message(informational, step('A')),
% step A
revise_model([], [], ACTL, Et, Ut, [A | At])
print_message(informational, step('A'))
;
print_message(informational, step('A''')),
% step A'
% try to find some rule from the trace and delete it
fail
).
find_and_delete_rules,
% FIXME check At too since self-loops can be added by removing a reaction
append([A | Ut], Et, AllSpec),
recheck_spec(AllSpec, Init, Bool)
),
revise_model([], [], ACTL, Et, Ut, [A | At]).
revise_model([], [], [], _, _, _) :-
......@@ -98,6 +84,12 @@ revise_model([], [], [], _, _, _) :-
print_message(informational, success(Reactions)).
recheck_spec(Specs, Init, Bool) :-
join_op('/\\', Specs, Spec),
print_message(informational, checking(Spec)),
check_ctl_impl(Spec, Init, no, Bool, true).
categorize_query(Q1 /\ Q2, ECTL, UCTL, ACTL) :-
!,
categorize_query(Q1, E1, U1, A1),
......@@ -164,6 +156,11 @@ is_ectl(Q) :-
).
find_and_add_rule :-
find_rule(R),
print_message(informational, trying(R)),
add_reaction_backtracking(R).
% TODO use a pattern instead of fixing S =[E]=> P
find_rule(R) :-
enumerate_all_molecules(Molecules),
......@@ -195,6 +192,12 @@ add_reaction_backtracking(R) :-
fail
).
find_and_delete_rules :-
listing(nusmv:trace/1),
fail.
prolog:message(step(Step)) -->
['Entering step ~w'-[Step]].
......
......@@ -43,4 +43,18 @@ test(
findall(Item, item([kind: reaction, item: Item]), Reactions).
test(
'revise_model rule deletion for ACTL',
[
all(Reactions = [[]])
% condition(flag(slow_test, true, true)),
]
) :-
command(present(a)),
command(absent(b)),
biocham(add_reaction(a => b)),
revise_model('AG'(a)),
findall(Item, item([kind: reaction, item: Item]), Reactions).
:- end_tests(revision).
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