| fmtk: | |
 |
Formal Methods Toolkit:
A growing collection of containers and notebooks for working with specification languages & model checkers 
|
Formal Methods Toolkit: A growing collection of containers and notebooks for working with specification languages & model checkers
Under construction. This bundles a basic jupyterlab deployment with other containers, mostly using the Storm Model Checker official images for a base. Plus adding momba, CoSApp, and a (optional) Neo4j deployment.
This is for local experimentation, not deployment, and it isn't supposed to be secure. Servers are optional, but Jupyter is unauthenticated & Neo4j auth details are plaintext inside the project config.
See the Dockerfile, docker-compose.yml and notebooks/ for more details.
Build the container and run the smoke tests.
$ make clean build testYou can interact with the container in several ways, for example:
# Drop into an interactive shell for this container (bash)
$ make shell
# or, equivalently
$ docker compose run shell
# to send a specific command to the container,
# args are still passed to bash so use something like:
$ docker compose run shell -x -c 'storm --version || true'The docker-compose.yml will mount the working-directory for you automatically to give access to any model files.
You can interact with the storm CLI directly like this:
$ docker compose run storm --version
Storm 1.8.0
Date: Sun Apr 14 01:12:54 2024
Command line arguments: --version
Current working directory: /workspace
Compiled on Linux 5.15.49-linuxkit using gcc 12.2.0 with flags ' -O3 -DNDEBUG -fprefetch-loop-arrays -flto -flto-partition=none -fomit-frame-pointer'
Linked with GNU Linear Programming Kit v5.0.
Linked with Microsoft Z3 Optimizer v4.8 Build 12 Rev 0.
Linked with CArL.You can also drop into an IPython shell inside the container, and then interact directly with stormpy. See also the stormpy tutorial here.
$ docker compose run stormpy
+ ipython -i -c 'import stormpy; print(stormpy.__version__)'
Python 3.11.2 (main, May 30 2023, 17:45:26) [GCC 12.2.0]
Type 'copyright', 'credits' or 'license' for more information
IPython 8.23.0 -- An enhanced Interactive Python. Type '?' for help.
1.8.0
In [1]: import stormpy.examples.files
In [2]: from stormpy.examples import files
In [3]: dir(files)
Out[3]:
['dft_galileo_hecs',
'dft_json_and',
'drn_ctmc_dft',
'drn_pdtmc_die',
'drn_pomdp_maze',
'gspn_pnml_simple',
'gspn_pnpro_simple',
'jani_dtmc_die',
'prism_dtmc_brp',
'prism_dtmc_die',
'prism_ma_simple',
'prism_mdp_coin_2_2',
'prism_mdp_firewire',
'prism_mdp_maze',
'prism_mdp_slipgrid',
'prism_par_pomdp_maze',
'prism_pdtmc_brp',
'prism_pdtmc_die',
'prism_pmdp_coin_two_dice',
'prism_pomdp_maze',]# starts jupyter lab for this container
$ make serve
# or, equivalently
$ docker compose up lab
# or, with daemonization
$ make serve/bg
# this will open a browser for the lab notebooks:
$ make open
# stop the container
$ make stopYou can also run notebooks, inside the main container, but outside of jupyterlab's web interface:
$ notebook=./notebooks/jani-model.ipynb make run# Start GraphDB
$ docker compose up -d neo4j
# opens WebUI (http://localhost:7474/) in browser
$ make open/neo4j
# get a interactive Cypher shell:
$ docker compose run -T cypher
# use Cypher with pipes
$ echo 'MATCH (n) return n;' | docker compose run -T cypher
# purge graphdb
$ echo 'MATCH (n) DETACH DELETE n;' | docker compose run -T cypher
# run a notebook that does stuff with neo
$ notebook=notebooks/neo4j-driver.ipynb make run