Commit c6791a7e authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

better testing/display

parent 2f1067f8
......@@ -29,26 +29,26 @@ revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
(
check_ctl_impl(U, Init, no, Bool, true)
->
write(step('U')),nl,
print_message(informational, step('U')),
% step U
revise_model([], UCTL, ACTL, Et, [U | Ut], At)
;
write(step('Up')),nl,
print_message(informational, step('U''')),
% step U'
% try to find some rule from the pattern
find_rule(R),
write(trying(R)),nl,
print_message(informational, trying(R)),
add_reaction_backtracking(R),
% FIXME check Et too since self-loops can be broken by adding a reaction
append([U | Ut], At, AllSpec),
join_op('/\\', AllSpec, Spec),
write(checking(Spec)),nl,
print_message(informational, checking(Spec)),
check_ctl_impl(Spec, Init, no, Bool, true)
->
revise_model([], UCTL, ACTL, Et, [U | Ut], At)
;
write(step('Upp')),nl,
% step U'''
print_message(informational, step('U''''')),
% step U''
% try to find some rule from the trace and delete it
fail
).
......@@ -59,11 +59,11 @@ revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
(
check_ctl_impl(E, Init, no, Bool, true)
->
write(step('E')),nl,
print_message(informational, step('E')),
% step E
revise_model(ECTL, UCTL, ACTL, [E | Et], Ut, At)
;
write(step('Ep')),nl,
print_message(informational, step('E''')),
% step E'
% try to find some rule from the pattern
find_rule(R),
......@@ -71,7 +71,7 @@ revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
% FIXME check Et too since self-loops can be broken by adding a reaction
append([E | Ut], At, AllSpec),
join_op('/\\', AllSpec, Spec),
write(checking(Spec)),nl,
print_message(informational, checking(Spec)),
check_ctl_impl(Spec, Init, no, Bool, true),
revise_model(ECTL, UCTL, ACTL, [E | Et], Ut, At)
).
......@@ -82,11 +82,11 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
(
check_ctl_impl(A, Init, no, Bool, true)
->
write(step('A')),nl,
print_message(informational, step('A')),
% step A
revise_model([], [], ACTL, Et, Ut, [A | At])
;
write(step('Ap')),nl,
print_message(informational, step('A''')),
% step A'
% try to find some rule from the trace and delete it
fail
......@@ -94,7 +94,8 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
revise_model([], [], [], _, _, _) :-
write(success),nl.
findall(Item, item([kind: reaction, item: Item]), Reactions),
print_message(informational, success(Reactions)).
categorize_query(Q1 /\ Q2, ECTL, UCTL, ACTL) :-
......@@ -186,10 +187,28 @@ find_rule(R) :-
add_reaction_backtracking(R) :-
(
add_item([kind: reaction, item: R]),
list_reactions,nl,
write(added(R)),nl
% list_reactions,nl,
print_message(informational, added(R))
;
delete_item([kind: reaction, item: R]),
write(removed(R)),nl,
print_message(informational, removed(R)),
fail
).
prolog:message(step(Step)) -->
['Entering step ~w'-[Step]].
prolog:message(added(Reaction)) -->
['Adding reaction ~w'-[Reaction]].
prolog:message(removed(Reaction)) -->
['Failed', nl, 'Removing reaction ~w'-[Reaction]].
prolog:message(trying(Reaction)) -->
['Considering reaction ~w'-[Reaction]].
prolog:message(checking(Query)) -->
['Checking consolidated query ~w'-[Query]].
prolog:message(success(Reactions)) -->
['Success!', nl, 'The new model is: ~w'-[Reactions]].
......@@ -18,7 +18,20 @@ test(
).
test(
'revise_model',
'revise_model rule addition for ECTL',
[
all(Reactions = [['_' => b], ['_' =[a]=> b], [a => b]])
% condition(flag(slow_test, true, true)),
]
) :-
command(present(a)),
command(absent(b)),
revise_model('EU'(a, b)),
findall(Item, item([kind: reaction, item: Item]), Reactions).
test(
'revise_model rule addition for UCTL',
[
all(Reactions = [[a => b]])
% condition(flag(slow_test, true, true)),
......@@ -26,7 +39,7 @@ test(
) :-
command(present(a)),
command(absent(b)),
revise_model('EF'(b /\ not(a))),
revise_model('EF'(b /\ 'AG'(not(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