Commit cd620813 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

added -> to CTL, and separated grammar

parent e1ea2c63
:- module(
nusmv,
[
% grammar
ctl/1,
op(800, xfy, '/\\'),
op(900, xfy, '\\/'),
% options
nusmv_initial_states/1,
nusmv_counter_example/1,
......@@ -20,50 +16,9 @@
% Only for separate compilation/linting
:- use_module(reaction_rules).
:- use_module(ctl).
:- grammar(ctl).
ctl('EX'(E)) :-
ctl(E).
ctl('EF'(E)) :-
ctl(E).
ctl('EG'(E)) :-
ctl(E).
ctl('EU'(E, F)) :-
ctl(E),
ctl(F).
ctl('AX'(E)) :-
ctl(E).
ctl('AF'(E)) :-
ctl(E).
ctl('AG'(E)) :-
ctl(E).
ctl('AU'(E, F)) :-
ctl(E),
ctl(F).
ctl(not(E)) :-
ctl(E).
ctl(E /\ F) :-
ctl(E),
ctl(F).
ctl(E \/ F) :-
ctl(E),
ctl(F).
ctl(E) :-
object(E).
export_nusmv(OutputFile) :-
biocham_command,
type(OutputFile, output_file),
......@@ -564,6 +519,12 @@ check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :-
).
translate_ctl_for_nusmv(A -> B, Atom) :-
!,
translate_ctl_for_nusmv(A, AA),
translate_ctl_for_nusmv(B, BB),
atomic_list_concat(['(!', AA, ' | ', BB, ')'], Atom).
translate_ctl_for_nusmv(A \/ B, Atom) :-
!,
translate_ctl_for_nusmv(A, AA),
......
......@@ -16,7 +16,7 @@ test(
true(Result == 'false')
]
) :-
nusmv:check_ctl_impl('AG'(not(c) \/ b), all, no, negative, Result).
nusmv:check_ctl_impl('AG'(c -> b), all, no, negative, Result).
test('export_infl', [setup(set_a_dummy_influence_model), cleanup(clear_model)]) :-
......
......@@ -15,7 +15,7 @@ revise_model(Query) :-
type(Query, ctl),
doc(
'Use theory-revision on the current model to satisfy the query given as
argument. cf. \\cite{CCFS05tcsb}.'
argument. cf. \\texttt{CCFS05tcsb}.'
),
categorize_query(Query, ECTL, UCTL, ACTL),
retractall(need_recheck),
......
:- use_module(library(plunit)).
% not necessary, except for separate compilation
:- use_module(reaction_rules).
:- use_module(ctl).
:- begin_tests(revision).
% condition(flag(slow_test, true, true)),
......
......@@ -21,6 +21,7 @@
- influence_rules.pl
* Syntax of Biocham Temporal Specifications
** Boolean temporal properties
- ctl.pl
** Numerical temporal properties
* Commands at Top-level
- toplevel.pl
......
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