Commit 0eb4699d authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

added CTL spec as a first class citizen

parent 73b1bc15
...@@ -4,6 +4,11 @@ ...@@ -4,6 +4,11 @@
% grammar % grammar
ctl/1, ctl/1,
% command % command
add_ctl/1,
delete_ctl/1,
delete_ctl/0,
list_ctl/0,
% API
normalize_query/3 normalize_query/3
] ]
). ).
...@@ -69,6 +74,35 @@ ctl(E) :- ...@@ -69,6 +74,35 @@ ctl(E) :-
object(E). object(E).
add_ctl(Formula) :-
biocham_command,
type(Formula, ctl),
doc('Adds a CTL formula to the currently declared CTL specification.'),
add_item([kind: ctl_spec, item: Formula]).
delete_ctl(Formula) :-
biocham_command,
type(Formula, ctl),
doc('Removes a CTL formula to the currently declared CTL specification.'),
find_item([id: Id, type: ctl_spec, item: Formula]),
delete_item(Id).
delete_ctl :-
biocham_command,
doc('Removes all formulae from the current CTL specification.'),
% model: current_model?
delete_items([kind: ctl_spec]).
list_ctl :-
biocham_command,
doc('Prints out all formulae from the current CTL specification.'),
% model: current_model?
list_items([kind: ctl_spec]).
normalize_query(Query, NQuery, SLeaves) :- normalize_query(Query, NQuery, SLeaves) :-
normalize_query(Query, NQuery, [], Leaves), normalize_query(Query, NQuery, [], Leaves),
sort(Leaves, SLeaves). sort(Leaves, SLeaves).
......
...@@ -8,6 +8,7 @@ ...@@ -8,6 +8,7 @@
% commands % commands
export_nusmv/1, export_nusmv/1,
check_ctl/1, check_ctl/1,
check_ctl/0,
% API % API
check_ctl_impl/5, check_ctl_impl/5,
enumerate_all_molecules/1 enumerate_all_molecules/1
...@@ -15,6 +16,7 @@ ...@@ -15,6 +16,7 @@
). ).
:- use_module(ctl). :- use_module(ctl).
:- use_module(util).
% Only for separate compilation/linting % Only for separate compilation/linting
:- use_module(reaction_rules). :- use_module(reaction_rules).
...@@ -537,6 +539,15 @@ check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :- ...@@ -537,6 +539,15 @@ check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :-
). ).
check_ctl :-
biocham_command,
doc('Checks the current CTL specification (i.e., the conjunction of all
formulae of the current specification).'),
findall(Formula, item([kind: ctl_spec, item: Formula]), Specs),
join_op('/\\', Specs, Spec),
check_ctl(Spec).
translate_ctl_for_nusmv(A -> B, Atom) :- translate_ctl_for_nusmv(A -> B, Atom) :-
!, !,
translate_ctl_for_nusmv(A, AA), translate_ctl_for_nusmv(A, AA),
......
:- module( :- module(
revision, revision,
[ [
revise_model/1 revise_model/1,
revise_model/0
] ]
). ).
...@@ -24,6 +25,15 @@ revise_model(Query) :- ...@@ -24,6 +25,15 @@ revise_model(Query) :-
print_message(informational, removed(Removed)). print_message(informational, removed(Removed)).
revise_model :-
biocham_command,
doc('Use theory-revision as above, using the currently defined CTL
specification.'),
findall(Formula, item([kind: ctl_spec, item: Formula]), Specs),
join_op('/\\', Specs, Spec),
revise_model(Spec).
revise_model(Query, Added, Removed) :- revise_model(Query, Added, Removed) :-
findall(Item, item([kind: reaction, item: Item]), Reactions), findall(Item, item([kind: reaction, item: Item]), Reactions),
nb_setval(need_recheck, false), nb_setval(need_recheck, false),
......
...@@ -118,7 +118,7 @@ test( ...@@ -118,7 +118,7 @@ test(
assertion(Removed = [a=>'_', b=>'_', c=>'_']). assertion(Removed = [a=>'_', b=>'_', c=>'_']).
test( test(
'Qu', 'Qu1',
[ [
setup(clear_model) setup(clear_model)
] ]
...@@ -135,4 +135,34 @@ test( ...@@ -135,4 +135,34 @@ test(
assertion(Removed = [k1 for '_' => 'CycB']). assertion(Removed = [k1 for '_' => 'CycB']).
test(
'Qu2',
[
blocked(tooslow),
setup(clear_model)
]
) :-
command(load('library:examples/cell_cycle/Qu_et_al_2003.bc')),
command(add_ctl('AG'(not('CycB-CDK~{p1}')->checkpoint('C25~{p1,p2}','CycB-CDK~{p1}')))),
command(add_ctl(reachable('CycB'))),
command(add_ctl(reachable('CycB-CDK~{p1,p2}'))),
command(add_ctl(reachable('C25'))),
command(add_ctl(reachable('C25~{p1}'))),
command(add_ctl(reachable('C25~{p1,p2}'))),
findall(Formula, item([kind: ctl_spec, item: Formula]), Specs),
join_op('/\\', Specs, Spec),
once(
revision:revise_model(
Spec,
Added,
Removed
)
),
assertion(Added == []),
assertion(Removed = [
k5*['CycB-CDK~{p1,p2}']for'CycB-CDK~{p1,p2}'=>'CycB-CDK~{p1}',
k15*['CKI-CycB-CDK~{p1}'] for 'CKI-CycB-CDK~{p1}'=>'CKI'+'CycB-CDK~{p1}'
]).
:- end_tests(revision). :- 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