You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
PosetLogic is a model checker on Kappa causal flows (stories). It is designed to be used as an accompaying analysis tool for a KaSim simulation. Users can write influence statements about a Kappa model and PosetLogic will query the pool of stories to check if there exists a 'mechanistic' explanation of the influence statement.
3
+
4
+
## Installation
5
+
6
+
To compile PosetLogic you need
7
+
8
+
- the OCaml native compiler version 4.02.3 or above as well as _ocamlbuild_, _findlib_ and _Yojson_ library.
9
+
- the KappaLib that you can get from https://github.com/Kappa-Dev/KaSim
10
+
11
+
If you use opam KappaLib, OCaml compilers, ocamlbuild and findlib are provided by it.
12
+
13
+
## Usage
14
+
15
+
You first need a pool of Kappa stories in a json format. You can produce them by running a KaSim simulation (please visit Kappa's documentation on http://dev.executableknowledge.org/docs/KaSim-manual-master/KaSim_manual.htm). Or you can use the stories provided in the example set.
16
+
17
+
Then you need to write a formula file. Each line in the file is either a formula or a variable assignation.
18
+
19
+
## Run the example
20
+
21
+
In the folder [examples] you'll find the set of stories produced by the model test3.ka with the simulation options of inputs.ka. The stories are both in a json format (necessary for PosetLogic) and in a dot format, for visualisation. The files test1 and test2 are files with formulas.
22
+
23
+
You can test whether the model in test3.ka satisfies the formulas in the files test1 and test2 by typing
0 commit comments