Commit 7dbe8a80 authored by Sylvain Soliman's avatar Sylvain Soliman

comments and typos

parent d6cd76d5
......@@ -61,9 +61,9 @@ revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
(
check_ctl_impl(E, Init, no, Bool, true)
->
debug(revision, 'Entering step w', ['E'])
debug(revision, 'Entering step ~w', ['E'])
;
debug(revision, 'Entering step w', ['E''']),
debug(revision, 'Entering step ~w', ['E''']),
find_and_add_rule,
% FIXME check Et too since self-loops can be broken by adding a reaction
append([E | Ut], At, AllSpec),
......@@ -77,15 +77,15 @@ revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
(
check_ctl_impl(U, Init, no, Bool, true)
->
debug(revision, 'Entering step w', ['U'])
debug(revision, 'Entering step ~w', ['U'])
;
(
debug(revision, 'Entering step w', ['U''']),
debug(revision, 'Entering step ~w', ['U''']),
find_and_add_rule,
% FIXME check Et too since self-loops can be broken by adding a reaction
append([U | Ut], At, AllSpec)
;
debug(revision, 'Entering step w', ['U''''']),
debug(revision, 'Entering step ~w', ['U''''']),
delete_rules,
% FIXME check At too since self-loops can be added by removing a reaction
append([U | Ut], Et, AllSpec)
......@@ -101,17 +101,20 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
(
Result = true
->
debug(revision, 'Entering step w', ['A']),
debug(revision, 'Entering step ~w', ['A']),
% 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])
;
debug(revision, 'Entering step w', ['A''']),
debug(revision, 'Entering step ~w', ['A''']),
(
% always true? Not sure we always have a counter-example
nusmv:trace(_)
->
% might not be enough to make A true, thus we do not add A to the
% treated formulae
delete_rules_from_trace
;
delete_rules,
......
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