Skip to content
Snippets Groups Projects
Commit e7ee99e9 authored by Dave Parker's avatar Dave Parker
Browse files

Merge branch 'prism'

parents bd78314e f6a2620b
No related branches found
No related tags found
No related merge requests found
Showing
with 109 additions and 11 deletions
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="src" path="prism/src"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER">
<attributes>
<attribute name="module" value="true"/>
</attributes>
</classpathentry>
<classpathentry kind="src" path="prism/unit-tests"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/5"/>
<classpathentry kind="lib" path="prism/lib/epsgraphics.jar"/>
<classpathentry kind="lib" path="prism/lib/jcommon.jar"/>
<classpathentry kind="lib" path="prism/lib/jfreechart.jar"/>
......
......@@ -25,4 +25,5 @@ jobs:
working-directory: ./prism
run: |
make
make unittests
make tests
mdp
const double p = 1e-13;
module rare
rare : bool init false;
[tick] !rare -> p: (rare' = true)
+ 1-p: true;
[tick] rare -> true;
endmodule
rewards
rare: 1-p;
!rare: p;
// [tick] rare: 1-p;
// [tick] !rare: p;
endrewards
\ No newline at end of file
-explicit
-mtbdd
-sparse
-hybrid
\ No newline at end of file
# Reduce precision for some tests due to minor differences between the engines
-exportmodelprecision 16 -exportmodel rare.nm.tra
-exportmodelprecision 16 -exportmodel rare.nm.srew
-exportmodelprecision 16 -mdp -importmodel rare.nm.sta,tra,srew -exportmodel rare.nm.tra
-exportmodelprecision 16 -mdp -importmodel rare.nm.sta,tra,srew -exportmodel rare.nm.srew
// RESULT (p=1e-13): 1.0
Pmax=? [F rare];
// RESULT (p=1e-13): true
0.99 <= Rmin=? [F rare];
-gs
\ No newline at end of file
2 2
0 1e-13
1 0.9999999999999
(rare)
0:(false)
1:(true)
2 2 3
0 0 0 0.9999999999999 tick
0 0 1 1e-13 tick
1 0 1 1 tick
2 2
0 0 1e-13
1 1 0.9999999999999
dtmc
const double p = 1e-13;
module rare
rare : bool init false;
[tick] !rare -> p: (rare' = true)
+ 1-p: true;
[tick] rare -> true;
endmodule
rewards
rare: 1-p;
!rare: p;
// [tick] rare: 1-p;
// [tick] !rare: p;
endrewards
\ No newline at end of file
-explicit
-mtbdd
-sparse
-hybrid
\ No newline at end of file
# Reduce precision for some tests due to minor differences between the engines
-exportmodelprecision 16 -exportmodel rare.pm.tra
-exportmodelprecision 16 -exportmodel rare.pm.srew
-exportmodelprecision 16 -dtmc -importmodel rare.pm.sta,tra,srew -exportmodel rare.pm.tra
-exportmodelprecision 16 -dtmc -importmodel rare.pm.sta,tra,srew -exportmodel rare.pm.srew
// RESULT (p=1e-13): 1.0
P=? [F rare];
// RESULT (p=1e-13): true
R>=0.99 [F rare];
2 2
0 1e-13
1 0.9999999999999
(rare)
0:(false)
1:(true)
2 3
0 0 0.9999999999999
0 1 1e-13
1 1 1
2 2
0 0 1e-13
1 1 0.9999999999999
# Reduce precision for some tests due to minor differences between the engines
# Export all model info in different formats
-exportmodel cluster.sm.all
-exportmodel cluster.sm.mrmc.all:mrmc
-exportmodel cluster.sm.matlab.all:matlab
-exportmodel cluster.sm.rows.all:rows
-exportmodelprecision 16 -exportmodel cluster.sm.all
-exportmodelprecision 16 -exportmodel cluster.sm.mrmc.all:mrmc
-exportmodelprecision 16 -exportmodel cluster.sm.matlab.all:matlab
-exportmodelprecision 16 -exportmodel cluster.sm.rows.all:rows
# Export model info separately (for a few formats)
-exportmodel cluster.sm.tra
-exportmodelprecision 16 -exportmodel cluster.sm.tra
-exportmodel cluster.sm.lab
-exportmodel cluster.sm.sta
-exportmodel cluster.sm.srew
-exportmodel cluster.sm.trew
-exportmodel cluster.sm.mrmc.tra:mrmc
-exportmodelprecision 16 -exportmodel cluster.sm.mrmc.tra:mrmc
-exportmodel cluster.sm.mrmc.lab:mrmc
-exportmodel cluster.sm.mrmc.sta:mrmc
-exportmodel cluster.sm.mrmc.srew:mrmc
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment