Commit 7797eab0 authored by Maxime Perrotin's avatar Maxime Perrotin

Update README

parent 7f16c91a
TASTE MODEL CHECKER
===
(c) 2017-2018 European Space Agency / Maxime Perrotin (c) 2017-2018 European Space Agency / Maxime Perrotin
This repository contains all the components of the [future] TASTE Model Checker. This repository contains the components related to the model checker developed for TASTE.
There are currently two main components under development: `taste-properties` and `asn1-iterators`
taste-properties
---
The `taste-properties` package is a Python application that is needed to parse and compile properties corresponding to a stop condition.
It is closely linked to SDL models and the parser is based on the parser from Opengeode.
A `property` is essentially an expression that can be evaluated to `true` or `false` during the execution of a program (e.g. a TASTE function). A `stop condition` is partly what the model checker is looking for to decide if the model is valid or not. Example of stop conditions that can be processed by `taste-properties`:
* stop if x>10;
* stop if trafficlight = red and state /= stopped
The actual inputs of `taste-properties` are :
1. A **SDL** model from Opengeode (`.pr`)
2. A property file containing one or more stop conditions.
For example, assuming you have a file named `properties` and containing some stop conditions that reference the state and variables of a SDL model named orchestrator.pr, you can run:
$ taste-properties -s properties orchestrator.pr
This will have the effect of creating a number of files, including one named `Makefile.properties`. This will build up a library containing a compiled version of the library. In our case, `liborchestrator_stop_conditions.so`. This file can be used by the Opengeode simulator, if you copy the file in the simulation folder and run the simulator with the following command:
$ opengeode-simulator -p properties
During the simulation, after each step the properties are evaluated and a pop-up is displayed if any of them is evaluated to true.
asn1-iterators
---
After installing asn1-iterators, make sure you export After installing asn1-iterators, make sure you export
......
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