Commit eeed383e authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

bugfix some inconsistencies in mapk.bc, added a test to nusmv ctl_check

parent c3fcfae0
......@@ -15,13 +15,13 @@ RAF + RAFK <=> RAF-RAFK.
RAF~{p1} + RAFPH <=> RAF~{p1}-RAFPH.
MEK~{} + RAF~{p1} <=> MEK~{}-RAF~{p1}.
MEK + RAF~{p1} <=> MEK-RAF~{p1}.
MEK~{p1} + RAF~{p1} <=> MEK~{p1}-RAF~{p1}.
MEKPH + MEK~{p1} <=> MEK~{p1}-MEKPH.
MEKPH + MEK~{p1,p2} <=> MEK~{p1,p2}-MEKPH.
MAPK~{} + MEK~{p1,p2} <=> MAPK~{}-MEK~{p1,p2}.
MAPK + MEK~{p1,p2} <=> MAPK-MEK~{p1,p2}.
MAPK~{p1} + MEK~{p1,p2} <=> MAPK~{p1}-MEK~{p1,p2}.
MAPKPH + MAPK~{p1} <=> MAPK~{p1}-MAPKPH.
......
......@@ -351,6 +351,8 @@ make_nusmv_name(Molecule, Name) :-
atomic_list_concat(TranslatedList, Name).
translate_char(' ', '_').
translate_char('_', '__').
translate_char(',', '_c').
......
......@@ -34,21 +34,44 @@ test(
test(
'Lotka-Voltera',
[
forall(member(File, ['library:examples/lotka_voltera/LVr.bc',
'library:examples/lotka_voltera/LVi.bc'])),
setup(load(File)),
cleanup(clear_model)
]
'Lotka-Voltera',
[
forall(member(File, [
'library:examples/lotka_voltera/LVr.bc',
'library:examples/lotka_voltera/LVi.bc'
])),
setup(load(File)),
cleanup(clear_model)
]
) :-
assertion(nusmv:check_ctl_impl('EG'('R') /\ 'P', all, no, negative, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'('R' /\ not('P'))), all, no,
negative, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'(not('R') /\ not('P'))), all, no,
negative, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'(not('R') /\ 'P')), all, no,
negative, false)).
test(
'MAPK',
[
condition(flag(slow_test, true, true)),
true(Result == 'true')
]
) :-
assertion(nusmv:check_ctl_impl('EG'('R') /\ 'P', all, no, negative, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'('R' /\ not('P'))), all, no,
negative, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'(not('R') /\ not('P'))), all, no,
negative, true)),
assertion(nusmv:check_ctl_impl('EF'('AG'(not('R') /\ 'P')), all, no,
negative, false)).
command(clear_model),
command(load('library:examples/mapk/mapk.bc')),
nusmv:check_ctl_impl(
reachable('MAPK~{p1,p2}') /\
checkpoint('MEK~{p1}', 'MAPK~{p1,p2}') /\
'EF'('MEK~{p1}-MEKPH' /\ 'EF'('MAPK~{p1,p2}')) /\
'EU'(not('MEK~{p1}-MEKPH'), 'MAPK~{p1,p2}'),
all,
no,
negative,
Result
).
set_a_dummy_reaction_model :-
......
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