Commit e1ea2c63 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

full algorithm is in now

parent 995af213
......@@ -18,6 +18,7 @@ revise_model(Query) :-
argument. cf. \\cite{CCFS05tcsb}.'
),
categorize_query(Query, ECTL, UCTL, ACTL),
retractall(need_recheck),
revise_model(ECTL, UCTL, ACTL, [], [], []).
......@@ -70,23 +71,23 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
Result = true
->
print_message(informational, step('A')),
revise_model([], [], ACTL, Et, Ut, [A | At])
% we only consider adding U' and E' when A is fully satisfied, thus moving
% a step from the A' step of the algorithm to the A step
% FIXME check At too since self-loops can be added by removing a reaction
check_and_split(Et, Ut, [], Ett, Utt, [], Eprime, Uprime, [], Init, Bool),
revise_model(Eprime, Uprime, ACTL, Ett, Utt, [A | At])
;
print_message(informational, step('A''')),
(
nusmv:trace(_)
->
delete_rules_from_trace,
% FIXME check At too since self-loops can be added by removing a reaction
append(Ut, Et, AllSpec)
delete_rules_from_trace
;
delete_rules,
% we delete blindly, so we need to check A now
append([A | Ut], Et, AllSpec)
% we delete blindly, so we need to check A now to avoid useless
% recursion
check_ctl_impl(A, Init, no, Bool, true)
),
% FIXME the published algorithm actually allows to not re-check, but
% simply split and add again to the formulae to be verified
recheck_spec(AllSpec, Init, Bool),
revise_model([], [], [A | ACTL], Et, Ut, At)
).
......@@ -105,6 +106,42 @@ recheck_spec(Specs, Init, Bool) :-
check_ctl_impl(Spec, Init, no, Bool, true).
:- dynamic(need_recheck/0).
check_and_split(E, U, A, Et, Ut, At, Ef, Uf, Af, Init, Bool) :-
(
retract(need_recheck)
->
check_and_split(E, Et, Ef, Init, Bool),
check_and_split(U, Ut, Uf, Init, Bool),
check_and_split(A, At, Af, Init, Bool)
;
Et = E,
Ut = U,
At = A,
Ef = [],
Uf = [],
Af = []
).
check_and_split([], [], [], _Init, _Bool).
check_and_split([F | Formulae], Ft, Ff, Init, Bool) :-
(
check_ctl_impl(F, Init, no, Bool, true)
->
Ft = [F | FFt],
Ff = FFf
;
Ft = FFt,
Ff = [F | FFf]
),
check_and_split(Formulae, FFt, FFf, Init, Bool).
categorize_query(Q1 /\ Q2, ECTL, UCTL, ACTL) :-
!,
categorize_query(Q1, E1, U1, A1),
......
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