Commit e1161655 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

first success

parent 7a7349c9
......@@ -13,7 +13,8 @@
export_nusmv/1,
check_ctl/1,
% API
check_ctl_impl/5
check_ctl_impl/5,
enumerate_all_molecules/1
]
).
......
......@@ -42,6 +42,7 @@ revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
% 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,
check_ctl_impl(Spec, Init, no, Bool, true)
->
revise_model([], UCTL, ACTL, Et, [U | Ut], At)
......@@ -64,13 +65,13 @@ revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
;
write(step('Ep')),nl,
% step E'
fail,
% 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),
write(checking(Spec)),nl,
check_ctl_impl(Spec, Init, no, Bool, true),
revise_model(ECTL, UCTL, ACTL, [E | Et], Ut, At)
).
......@@ -92,6 +93,9 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
).
revise_model([], [], [], _, _, _).
categorize_query(Q1 /\ Q2, ECTL, UCTL, ACTL) :-
!,
categorize_query(Q1, E1, U1, A1),
......@@ -171,6 +175,7 @@ find_rule(R) :-
add_reaction_backtracking(R) :-
(
add_item([kind: reaction, item: R]),
list_reactions,nl,
write(added(R)),nl
;
delete_item([kind: reaction, item: R]),
......
......@@ -16,7 +16,7 @@ test(
).
test(
'revise_model'
'revise_model' %, [condition(flag(slow_test, true, true))]
) :-
command(present(a)),
command(absent(b)),
......
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