diff options
| -rw-r--r-- | Assignment2/src/Dockerfile | 8 | ||||
| -rw-r--r-- | Assignment2/src/die.prism | 4 | ||||
| -rwxr-xr-x | Assignment2/src/entry.sh | 3 | ||||
| -rwxr-xr-x | Assignment2/src/repair.sh | 14 | ||||
| -rwxr-xr-x | Assignment2/src/start.sh | 9 |
5 files changed, 26 insertions, 12 deletions
diff --git a/Assignment2/src/Dockerfile b/Assignment2/src/Dockerfile index 4bec59e..a654427 100644 --- a/Assignment2/src/Dockerfile +++ b/Assignment2/src/Dockerfile @@ -1,7 +1,7 @@ FROM movesrwth/storm:travis RUN apt-get update -qq &&\ - apt-get install -qq --no-install-recommends python3-setuptools python3-pip &&\ + apt-get install -qq --no-install-recommends z3 python3-setuptools python3-pip &&\ pip3 install pytest RUN mkdir /opt/pycarl &&\ @@ -24,4 +24,8 @@ RUN apt-get update -qq &&\ ENV CLEAN_HOME=/opt/clean ENV PATH=$PATH:/opt/storm/build/bin:/opt/clean/bin:/opt/clean/exe -ENTRYPOINT /src/entry.sh + +COPY DTMC.dcl DTMC.icl Z3.dcl Z3.icl Expression.dcl Expression.icl /tmp/ +RUN cd /tmp; clm -ms -b -nt -IL Platform DTMC -o dtmc + +ENTRYPOINT ["/src/repair.sh"] diff --git a/Assignment2/src/die.prism b/Assignment2/src/die.prism index 4c8d0de..45442d6 100644 --- a/Assignment2/src/die.prism +++ b/Assignment2/src/die.prism @@ -1,12 +1,10 @@ dtmc -const double p; - module die s : [0..7] init 0; d : [0..6] init 0; - [] s=0 -> p : (s'=1) + (1-p) : (s'=2); + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); diff --git a/Assignment2/src/entry.sh b/Assignment2/src/entry.sh deleted file mode 100755 index 3702ac5..0000000 --- a/Assignment2/src/entry.sh +++ /dev/null @@ -1,3 +0,0 @@ -cd /src -clm -ms -IL Platform -nr -nt DTMC -o dtmc -bash diff --git a/Assignment2/src/repair.sh b/Assignment2/src/repair.sh new file mode 100755 index 0000000..24cbb37 --- /dev/null +++ b/Assignment2/src/repair.sh @@ -0,0 +1,14 @@ +#!/bin/bash + +# Usage: repair.sh MODEL.prism PROPS.properties +MODEL="$1" +DRN="${MODEL/prism/drn}" +PROPS="$2" + +echo "Arguments: $@" + +echo "Generating DRN..." +storm --prism "$MODEL" --io:exportexplicit "$DRN" || exit + +echo "Repairing model..." +./dtmc "$DRN" "$PROPS" diff --git a/Assignment2/src/start.sh b/Assignment2/src/start.sh index d07316f..32072b5 100755 --- a/Assignment2/src/start.sh +++ b/Assignment2/src/start.sh @@ -1,13 +1,14 @@ #!/bin/bash -DOCKER_IMAGE=stormpy -DOCKER_NAME=stormpy +DOCKER_IMAGE=modelrepair +DOCKER_NAME=modelrepair docker build -q -t $DOCKER_IMAGE . || exit docker run\ --mount type=bind,source="$PWD",target=/src\ - -w /opt/storm/build/bin\ + -w /src\ --rm\ -it\ --name $DOCKER_NAME\ - $DOCKER_IMAGE + $DOCKER_IMAGE\ + $@ |