Use case: Stable states and model checking
Closed this issue · 9 comments
A first use case to implement would be :
- From a GINsim model, compute its sable states,
- Export in NuSMV format,
- Check a set of properties using NuSMV.
Started a first implementation using SnakeMake.
Workflow done, to be tested. Comments are welcome.
Commit of a draft Jupyter notebook corresponding to the use case.
The current workflow is wrong for the model-checking part: it is not possible to check properties for different INIT in a single file : NuSMV makes the conjonction of all init statements, which in this case lead to unsatisfiable constraint, therefore, no initial state are considered, and all the properties become true (you can easily check that a property like SPEC (CycD=1 & CycD=0) is true in your smv file.
Given the properties, the way to fix this is to ask GINsim to not export the initial state (no INIT statement), and use implications on the initial state for the properties.
(SPEC condition_on_init -> property)
I'll start implement this next week using the new NuSMV/Colomoto python API.
@aurelien-naldi is it possible to ask ginsim to skip the INIT generation using the NuSMVConfig object?
I've started in the dev branch a new version of this notebook:
https://nbviewer.jupyter.org/github/colomoto/colomoto-docker/blob/dev/usecases/Usecase%20-%20Logical%20model%20of%20the%20mammalian%20cell%20cycle.ipynb
Main question (@chernan @aurelien-naldi ): any idea how the Cycle1 variable has been generated?
The SnakeMake was updated according to recent developments and suggestions. But I noticed that some of the properties are now evaluated as wrong even if they are exactly the same as in the original smv file.
Need to double check with @aurelien-naldi if the NuSMV export is done properly.
Maybe try by putting parentheses before the ->, I'm not sure of the priorities:
SPEC (condition1 & condition2 & ...) -> ...
Same result.
With the original smv file on http://ginsim.org/node/189
if I uncomment the first property, NuSMV says false which is consistent with the results using the SnakeMake worflow.
Therefore, I guess it is expected that some properties are false and others are true.
I close the bug related to SnakeMake workflow ; I suggest to close that one too.