From 138a49bc600d2ece1fc8a00ad6acbef296190063 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Fri, 6 Jul 2018 21:56:18 +0200
Subject: Remove run.py, add README
---
Assignment2/src/README | 25 +++++++++++++++++++++++++
Assignment2/src/run.py | 47 -----------------------------------------------
2 files changed, 25 insertions(+), 47 deletions(-)
create mode 100644 Assignment2/src/README
delete mode 100755 Assignment2/src/run.py
(limited to 'Assignment2')
diff --git a/Assignment2/src/README b/Assignment2/src/README
new file mode 100644
index 0000000..5fa6f9a
--- /dev/null
+++ b/Assignment2/src/README
@@ -0,0 +1,25 @@
+You can run this tool in Docker.
+All you need to do is run:
+
+ ./start.sh die.prism die.properties
+
+Which repairs the model in die.prism for the properties in die.properties.
+
+The first time, this will build the Docker image. This can take a while, and
+may seem to freeze your system, and no progress is reported (unless you remove
+the -q switch in start.sh). The next time will be faster.
+
+The result is a Z3 model which contains instantiations for variables like v0x1.
+These are the values that should be added to the probabilities of transitions
+(here from state 0 to state 1) to make the model satisfy. Additionally, there
+is a variable cost which is the cost of the reparation. By default, this is the
+Sum of Squared Errors measure. To change to the Number of Modified Transitions
+measure, change line 328 of DTMC.icl to:
+
+ # (config,dtmc) = repairConfig NumberModifiedTransitions dtmc
+
+To run Z3 with a minimisation goal, uncomment line 339 in the same line.
+Additionally, to approximate the cost as described in the discussion of the
+paper, add a line like this under line 338:
+
+ # w = addAssert z3 "(> 0.3 cost)" w
diff --git a/Assignment2/src/run.py b/Assignment2/src/run.py
deleted file mode 100755
index 94862bf..0000000
--- a/Assignment2/src/run.py
+++ /dev/null
@@ -1,47 +0,0 @@
-#!/usr/bin/env python3
-from argparse import ArgumentParser, FileType
-import stormpy
-
-# as in https://github.com/moves-rwth/stormpy/blob/master/examples//parametric_models/02-parametric-models.py, but no idea why
-import stormpy.info
-if stormpy.info.storm_ratfunc_use_cln():
- import pycarl.cln.formula
-else:
- import pycarl.gmp.formula
-
-def main():
- parser = ArgumentParser(description='Model Repair tool')
- parser.add_argument('--program', '-p', type=FileType('r'), required=True,
- help='Path to the PRISM program to check and repair')
- parser.add_argument('--properties', '-f', type=FileType('r'), required=True,
- help='Path to the properties to check')
- args = parser.parse_args()
-
- program = stormpy.parse_prism_program(args.program.name)
- properties = args.properties.read()
-
- properties = stormpy.parse_properties_for_prism_program(properties, program)
- model = stormpy.build_parametric_model(program, properties)
-
- print('Built a model with {} states and {} transitions'.format(
- model.nr_states, model.nr_transitions))
- params = model.collect_probability_parameters()
- print('Parameter(s): ' + ', '.join([str(p) for p in params]))
-
- for prop in properties:
- print('Checking:', prop)
-
- result = stormpy.model_checking(model, prop)
- init = model.initial_states[0]
- func = result.at(init)
-
- collector = stormpy.ConstraintCollector(model)
- print('Well-formed constraints:')
- for formula in collector.wellformed_constraints:
- print(formula.get_constraint())
- print('Graph preserving constraints:')
- for formula in collector.graph_preserving_constraints:
- print(formula.get_constraint())
-
-if __name__ == '__main__':
- main()
--
cgit v1.2.3