update README

.gitignore

@@ -4,6 +4,7 @@ __pycache__/
 prerequisites/
 
 .vscode
+.idea
 
 # OSX
-.DS_Store
+.DS_Store

README.md

@@ -49,6 +49,19 @@ docker pull randriu/paynt
 docker run --rm -it randriu/paynt
 python3 paynt.py --help
 ```
+You can make simple script or alias in .bashrc for easier usage
+
+```shell
+#!/bin/sh
+
+source /path/to/your/venv/bin/activate
+python3 /path/to/your/paynt.py "$@"
+deactivate
+```
+
+```shell
+alias paynt="source /path/to/your/venv/bin/activate && python3 /path/to/your/paynt.py"
+```
 
 
 ## Running PAYNT
@@ -75,7 +88,7 @@ Options associated with the synthesis of finite-state controllers (FSCs) for a P
 - ``--fsc-synthesis``: enables incremental synthesis of FSCs for a (Dec-)POMDP using iterative exploration of k-FSCs
 - ``--posterior-aware``: enables the synthesis of posterior aware FSCs
 
-SAYNT [6] and Storm associated options (pomdp-api branch of Storm and Stormpy are needed):
+SAYNT [6] and Storm associated options  (pomdp-api branch of Storm and Stormpy are needed):
 - ``--storm-pomdp``: enables the use of Storm features, this flag is necessary for the other options in this section to work
 - ``--iterative-storm INTEGER INTEGER INTEGER``: runs the SAYNT algorithm, the parameters represent overall timeout, paynt timeout, storm timeout respectivelly. The recommended parameters for 15 minute runtime are 900 60 10
 - ``--get-storm-result INTEGER``: runs PAYNT for specified amount of seconds and then runs Storm using the computed FSC at cut-offs
@@ -88,7 +101,7 @@ SAYNT [6] and Storm associated options (pomdp-api branch of Storm and Stormpy ar
 
 Other options:
 - ``--help``: shows the help message of the PAYNT and aborts
-- ``--export [drn|pomdp]``: exports the model to *.drn/*.pomdp and aborts
+- ``--export [jani|drn|pomdp]``: exports the model to *.drn/*.pomdp and aborts
 
 
 Here are various PAYNT calls:
@@ -114,12 +127,12 @@ deactivate
 For instance, here is a simple PAYNT call:
 
 ```shell
-python3 paynt/paynt.py --project cav21-benchmark/grid --sketch sketch.templ --properties easy.props hybrid
+python3 paynt.py models/archive/cav21-paynt/grid --props easy.props hybrid
 ```
 
-The `--project` option specifies the path to the benchmark folder: now we will investigate the __Grid__ model discussed in [1].
+Now we will investigate the __Grid__ model discussed in [1].
 PAYNT inspects the content of this folder and locates the required files for the synthesis process: the sketch and the specification list.
-In the example above, the sketch file is `cav21-benchmark/grid/sketch.templ` (in this case, `--sketch` option could have been omitted), the specification file is `cav21-benchmark/grid/easy.properties` and the sketch does not have undefined constants, only holes.
+In the example above, the sketch file is `models/archive/cav21-paynt/grid/sketch.templ` (in this case, `--sketch` option could have been omitted), the specification file is `models/archive/cav21-paynt/grid/easy.props` and the sketch does not have undefined constants, only holes.
 Finally, the last argument specifies the selected synthesis method: `hybrid`.
 
 ## Getting started with PAYNT 
@@ -129,11 +142,11 @@ Having the tool installed, you can quickly test it by navigating to the tool fol
 ```sh
 cd /home/cav21/synthesis
 source env/bin/activate
-python3 paynt/paynt.py --project cav21-benchmark/dpm-demo  --properties sketch.props --method hybrid
+python3 paynt.py models/archive/cav21-paynt/dpm-demo --method hybrid
 ```
 
 The syntax of the command is described in more detail in the following chapters of this README.
-For now, we can see that we ask PAYNT to look at the sketch (located in directory ``cav21-benchmark/dpm-demo``) for the dynamic power manager discussed in Section 2 in [1] and synthesize it wrt. specification in file ``cav21-benchmark/dpm-demo/sketch.props`` using the advanced hybrid approach.
+For now, we can see that we ask PAYNT to look at the sketch (located in directory ``models/archive/cav21-paynt/dpm-demo``) for the dynamic power manager discussed in Section 2 in [1] and synthesize it wrt. specification in file ``models/archive/cav21-paynt/dpm-demo/sketch.props`` using the advanced hybrid approach.
 The tool will print a series of log messages and, in the end, a short summary of the synthesis process, similar to the one below:
 
 ```
@@ -168,7 +181,7 @@ Running PAYNT produces a sequence of log and a summary printed at the end of the
 For instance, if we run
 
 ```sh
-python3 paynt/paynt.py --project cav21-benchmark/dpm-demo hybrid
+python3 paynt.py models/archive/cav21-paynt/dpm-demo --method hybrid
 ```
 we obtain the following summary:
 
@@ -228,7 +241,7 @@ In other words, the PM observes the queue occupancy of the intervals: [0, T<sub>
 The values of these levels are unknown and thus are defined using four holes.
 For each occupancy level, the PM changes to the associated power profile P<sub>1</sub>, ..., P<sub>4</sub> in {0,1,2}, where numbers 0 through 2 encode the profiles *sleeping*, *idle* and *active}*, respectively. 
 The strategy which profile to used for the particular occupy is also unknown and thus defined using another four holes. 
-Finally, the queue capacity Q<sub>max</sub> is also unknown and thus the sketch includes in total 9 holes.
+Finally, the queue capacity Q<sub>max</sub> is also unknown and thus the sketch includes in total 8 holes.
 In the sketch, the definition of the hole takes place outside of any module (typically in the beginning of the program) and must include its data type (int or double) as well as the domain:
 
 ```
@@ -248,7 +261,7 @@ hole double T3 in {0.6,0.7,0.8};
 hole int QMAX in {1,2,3,4,5,6,7,8,9,10};
 ```
 
-The following sketch fragment describes the module for the described power manager. The modules implementing other components of the server are omitted here for brevity -- the entire sketch is available in [this file](cav21-benchmark/dpm-demo/sketch.templ).
+The following sketch fragment describes the module for the described power manager. The modules implementing other components of the server are omitted here for brevity -- the entire sketch is available in [this file](models/archive/cav21-paynt/dpm-demo/sketch.templ).
 
 ```
 module PM
@@ -267,7 +280,7 @@ The resulting sketch describes a *design space* of 10 x 5 x 4 x 3<sup>4</sup> =
 
 The goal is to find the concrete power manager, i.e., the instantiation of the holes, that minimizes power consumption while the expected number of lost requests during the operation time of the server is at most 1. 
 In general, a specification is formalized as a list of temporal logic formulae in the [`PRISM` syntax](https://www.prismmodelchecker.org/manual/PropertySpecification/Introduction).
-Here is a specification available within the benchmark directory [here](cav21-benchmark/dpm-demo/sketch.properties):
+Here is a specification available within the benchmark directory [here](models/archive/cav21-paynt/dpm-demo/sketch.props):
 
 ```
 R{"requests_lost"}<= 1 [ F "finished" ]
@@ -297,7 +310,7 @@ hole assignment: P1=1,P2=2,P3=2,P4=2,T1=0.0,T3=0.8,QMAX=5
 The obtained optimal power manager has queue capacity 5 with thresholds (after rounding) at 0, 2 and 4.
 In addition, the power manager always maintains an active profile unless the request queue is empty, in which case the device is put into an idle state.
 This solution guarantees expected number of lost requests to be at most one and has the power consumption of 9,100 units. 
-To double-check that there are no controllers having expected power consumption less than 9100, we can modify the specification file `cav21-benchmark/dpm-demo/sketch.properties` as follows:
+To double-check that there are no controllers having expected power consumption less than 9100, we can modify the specification file `models/archive/cav21-paynt/dpm-demo/sketch.props` as follows:
 
 ```
 R{"requests_lost"} <= 1 [ F "finished" ]
@@ -322,15 +335,15 @@ from which we can see that PAYNT indeed proved non-existence of a better solutio
 We might further consider a more complex program sketch __Grid__ (discussed in [1]), where we synthesize controller for a robot in an unpredictable environment.
 
 ```shell
-python3 paynt/paynt.py --project cav21-benchmark/grid --properties easy.properties hybrid
+python3 paynt.py models/archive/cav21-paynt/grid --props easy.props --method hybrid
 ```
 
 This sketch describes a family of 65K members, where each member has, on average 1225 states.
 Even though this is a much larger family with much larger chains than in the sketch considered before, the pruning ability of the advanced hybrid approach allows PAYNT to handle this specification in a matter of seconds.
 Meanwhile, one-by-one enumeration
 
 ```shell
-python3 paynt/paynt.py --project cav21-benchmark/grid --properties easy.properties onebyone
+python3 paynt.py models/archive/cav21-paynt/grid --props easy.props --method onebyone
 ```
 might take up to 20 minutes.
 
@@ -346,5 +359,3 @@ python3 -m pytest --cov=./../paynt/ --cov-report term-missing test_synthesis.py
 ```
 This command prints the coverage report, displaying the resulting coverage for individual source files.
 Our tests currently cover more than `90%` of the source code lines, even though the result shows `82%` because `~10%` of the source code is only temporary functions for debugging purposes that have no functionality.
-
-

paynt.py

@@ -1,4 +1,4 @@
 import paynt.cli
 
 if __name__ == "__main__":
-    paynt.cli.main()
+    paynt.cli.main()