Commit 887cc31b authored by Sylvain Soliman's avatar Sylvain Soliman

LV examples from Francois

parent 298e93a4
present(R).
present(P).
set_parameter(k1=2).
set_parameter(k2=2).
set_parameter(k3=1).
k1*R*P for R,P -< R.
k1*R*P for R,P -> P.
k2*R for R->R.
k3*P for P-<P.
% check_ctl(EG(R/\P)).
% check_ctl(EF(AG(R /\ (not P)))).
% check_ctl(EF(AG((not R) /\ (not P)))).
% check_ctl(EF(AG((not R) /\ P))).
present(R).
present(P).
set_parameter(k1=2).
set_parameter(k2=2).
set_parameter(k3=1).
k1*R*P for R+P => 2*P.
k2*R for R => 2*R.
k3*P for P => _.
% check_ctl(EG(R/\P)).
% check_ctl(EF(AG(R /\ (not P)))).
% check_ctl(EF(AG((not R) /\ (not P)))).
% check_ctl(EF(AG((not R) /\ P))).
......@@ -33,6 +33,32 @@ test(
nusmv:check_ctl('AG'(not(c) \/ b), [], Result).
test(
'LVr.bc',
[
setup(load('library:examples/lotka_voltera/LVr.bc')),
cleanup(clear_model)
]
) :-
assertion(nusmv:check_ctl('EG'('R') /\ 'P', [], true)),
assertion(nusmv:check_ctl('EF'('AG'('R' /\ not('P'))), [], true)),
assertion(nusmv:check_ctl('EF'('AG'(not('R') /\ not('P'))), [], true)),
assertion(nusmv:check_ctl('EF'('AG'(not('R') /\ 'P')), [], false)).
test(
'LVi.bc',
[
setup(load('library:examples/lotka_voltera/LVi.bc')),
cleanup(clear_model)
]
) :-
assertion(nusmv:check_ctl('EG'('R') /\ 'P', [], true)),
assertion(nusmv:check_ctl('EF'('AG'('R' /\ not('P'))), [], true)),
assertion(nusmv:check_ctl('EF'('AG'(not('R') /\ not('P'))), [], true)),
assertion(nusmv:check_ctl('EF'('AG'(not('R') /\ 'P')), [], false)).
set_a_dummy_reaction_model :-
clear_model,
add_reaction(a => 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