Commit 7a7349c9 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

forgot to add the files

parent 1539a230
:- module(
revision,
[
revise_model/1
]
).
% Only for separate compilation/linting
:- use_module(nusmv).
:- use_module(util).
revise_model(Query) :-
biocham_command,
type(Query, ctl),
doc(
'Use theory-revision on the current model to satisfy the query given as
argument. cf. \\cite{CCFS05tcsb}.'
),
categorize_query(Query, ECTL, UCTL, ACTL),
revise_model(ECTL, UCTL, ACTL, [], [], []).
% Everything copied as much as possible from CCFS05tcsb
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(U, Init, no, Bool, true)
->
write(step('U')),nl,
% step U
revise_model([], UCTL, ACTL, Et, [U | Ut], At)
;
write(step('Up')),nl,
% step U'
% try to find some rule from the pattern
find_rule(R),
write(trying(R)),nl,
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),
check_ctl_impl(Spec, Init, no, Bool, true)
->
revise_model([], UCTL, ACTL, Et, [U | Ut], At)
;
write(step('Upp')),nl,
% step U'''
% try to find some rule from the trace and delete it
fail
).
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(E, Init, no, Bool, true)
->
write(step('E')),nl,
% step E
revise_model(ECTL, UCTL, ACTL, [E | 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),
check_ctl_impl(Spec, Init, no, Bool, true),
revise_model(ECTL, UCTL, ACTL, [E | Et], 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)
->
write(step('A')),nl,
% step A
revise_model([], [], ACTL, Et, Ut, [A | At])
;
write(step('Ap')),nl,
% step A'
% try to find some rule from the trace and delete it
fail
).
categorize_query(Q1 /\ Q2, ECTL, UCTL, ACTL) :-
!,
categorize_query(Q1, E1, U1, A1),
categorize_query(Q2, E2, U2, A2),
append(E1, E2, ECTL),
append(U1, U2, UCTL),
append(A1, A2, ACTL).
categorize_query(not(Q), ECTL, UCTL, ACTL) :-
!,
categorize_query(Q, ACTL, UCTL, ECTL).
categorize_query(Query, [], [Query], []) :-
object(Query),
!.
categorize_query(Q, ECTL, UCTL, ACTL) :-
(
is_ectl(Q)
->
ECTL = [Q],
UCTL = [],
ACTL = []
;
is_actl(Q)
->
ECTL = [],
UCTL = [],
ACTL = [Q]
;
ECTL = [],
UCTL = [Q],
ACTL = []
).
is_actl(not(Q)) :-
!,
is_ectl(Q).
is_actl(Q) :-
Q =.. [Functor | QQ],
(
memberchk(Functor, ['EX', 'EF', 'EG', 'EU'])
->
fail
;
maplist(is_actl, QQ)
).
is_ectl(not(Q)) :-
!,
is_actl(Q).
is_ectl(Q) :-
Q =.. [Functor | QQ],
(
memberchk(Functor, ['AX', 'AF', 'AG', 'AU'])
->
fail
;
maplist(is_ectl, QQ)
).
% TODO use a pattern
% FIXME check that the rule is not in the model already
find_rule(R) :-
enumerate_all_molecules(Molecules),
member(M1, Molecules),
member(M2, Molecules),
M1 \= M2,
R = '=>'(M1, M2).
add_reaction_backtracking(R) :-
(
add_item([kind: reaction, item: R]),
write(added(R)),nl
;
delete_item([kind: reaction, item: R]),
write(removed(R)),nl
).
:- use_module(library(plunit)).
:- begin_tests(revision).
test(
'categorize_query',
[
true((ECTL, UCTL, ACTL) == (['EF'(a)], ['EU'(a, 'AG'(b))], ['AG'(b)]))
]
) :-
revision:categorize_query(
'EF'(a) /\ 'AG'(b) /\ 'EU'(a, 'AG'(b)),
ECTL,
UCTL,
ACTL
).
test(
'revise_model'
) :-
command(present(a)),
command(absent(b)),
revise_model('EF'(b /\ not(a))).
:- 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