From 2ef1acd80227b9ad7952f45bc5f6e66614b88bd2 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 9 Jul 2018 15:53:59 +0200 Subject: [PATCH] Fast adaptive uniformisation: Fix for incomplete model exploration During model exploration of a CTMC, when using fast adaptive uniformisation, only the last part of an update (rate & successor state) is used, as the indexing of the outgoing transitions is buggy. We now store all outgoing transitions and handle the case of multiple choices/enabled commands in the CTMC. + two test cases --- prism-tests/bugfixes/ctmc-fau-1.sm | 11 ++++++ prism-tests/bugfixes/ctmc-fau-1.sm.props | 15 ++++++++ prism-tests/bugfixes/ctmc-fau-1.sm.props.args | 3 ++ prism-tests/bugfixes/ctmc-fau-2.sm | 11 ++++++ prism-tests/bugfixes/ctmc-fau-2.sm.props | 31 ++++++++++++++++ prism-tests/bugfixes/ctmc-fau-2.sm.props.args | 3 ++ .../explicit/FastAdaptiveUniformisation.java | 37 +++++++++++-------- 7 files changed, 95 insertions(+), 16 deletions(-) create mode 100644 prism-tests/bugfixes/ctmc-fau-1.sm create mode 100644 prism-tests/bugfixes/ctmc-fau-1.sm.props create mode 100644 prism-tests/bugfixes/ctmc-fau-1.sm.props.args create mode 100644 prism-tests/bugfixes/ctmc-fau-2.sm create mode 100644 prism-tests/bugfixes/ctmc-fau-2.sm.props create mode 100644 prism-tests/bugfixes/ctmc-fau-2.sm.props.args diff --git a/prism-tests/bugfixes/ctmc-fau-1.sm b/prism-tests/bugfixes/ctmc-fau-1.sm new file mode 100644 index 00000000..24c94e76 --- /dev/null +++ b/prism-tests/bugfixes/ctmc-fau-1.sm @@ -0,0 +1,11 @@ +// test case for fast adaptive uniformisation bug (ignoring transitions) + +ctmc + +module m1 + s: [0..2] init 0; + + [] s=0 -> 1:(s'=1) + 2:(s'=2); + [] s>0 -> 1:true; +endmodule + diff --git a/prism-tests/bugfixes/ctmc-fau-1.sm.props b/prism-tests/bugfixes/ctmc-fau-1.sm.props new file mode 100644 index 00000000..e8aca122 --- /dev/null +++ b/prism-tests/bugfixes/ctmc-fau-1.sm.props @@ -0,0 +1,15 @@ +const double T; + +// RESULT (T=1): 0.3167376343237416 +// RESULT (T=2): 0.332507070725914 +// RESULT (T=3): 0.33329218265878835 +// RESULT (T=4): 0.3333312759432579 +// RESULT (T=5): 0.33333321817286715 +P=? [ F=T s=1 ]; + +// RESULT (T=1): 0.6334752686474832 +// RESULT (T=2): 0.665014141451828 +// RESULT (T=3): 0.6665843653175767 +// RESULT (T=4): 0.6666625518865158 +// RESULT (T=5): 0.6666664363457 +P=? [ F=T s=2 ]; diff --git a/prism-tests/bugfixes/ctmc-fau-1.sm.props.args b/prism-tests/bugfixes/ctmc-fau-1.sm.props.args new file mode 100644 index 00000000..8485aa75 --- /dev/null +++ b/prism-tests/bugfixes/ctmc-fau-1.sm.props.args @@ -0,0 +1,3 @@ +-const T=1:1:5 -transientmethod unif +-const T=1:1:5 -transientmethod fau + diff --git a/prism-tests/bugfixes/ctmc-fau-2.sm b/prism-tests/bugfixes/ctmc-fau-2.sm new file mode 100644 index 00000000..636383ec --- /dev/null +++ b/prism-tests/bugfixes/ctmc-fau-2.sm @@ -0,0 +1,11 @@ +// test correct handling of multiple enabled commands in CTMC when using fast adaptive uniformisation + +ctmc + +module m1 + s: [0..4] init 0; + + [a] s=0 -> 1:(s'=1) + 2:(s'=2); + [b] s=0 -> 3:(s'=3) + 4:(s'=4); + [] s>0 -> 1:true; +endmodule diff --git a/prism-tests/bugfixes/ctmc-fau-2.sm.props b/prism-tests/bugfixes/ctmc-fau-2.sm.props new file mode 100644 index 00000000..9e3fce60 --- /dev/null +++ b/prism-tests/bugfixes/ctmc-fau-2.sm.props @@ -0,0 +1,31 @@ +const double T; + +// RESULT (T=0.2): 0.08646646794 +// RESULT (T=0.4): 0.09816843470 +// RESULT (T=0.6): 0.09975212121 +// RESULT (T=0.8): 0.09996644936 +// RESULT (T=1.0): 0.09999545617 +P=? [ F=T s=1 ]; + +// RESULT (T=0.2): 0.1729329358997 +// RESULT (T=0.4): 0.1963368694095 +// RESULT (T=0.6): 0.1995042424355 +// RESULT (T=0.8): 0.1999328987210 +// RESULT (T=1.0): 0.1999909123404 +P=? [ F=T s=2 ]; + + +// RESULT (T=0.2): 0.2593994038496 +// RESULT (T=0.4): 0.2945053041143 +// RESULT (T=0.6): 0.2992563636533 +// RESULT (T=0.8): 0.2998993480815 +// RESULT (T=1.0): 0.2999863685106 +P=? [ F=T s=3 ]; + + +// RESULT (T=0.2): 0.3458658717995 +// RESULT (T=0.4): 0.3926737388191 +// RESULT (T=0.6): 0.3990084848710 +// RESULT (T=0.8): 0.3998657974421 +// RESULT (T=1.0): 0.3999818246808 +P=? [ F=T s=4 ]; diff --git a/prism-tests/bugfixes/ctmc-fau-2.sm.props.args b/prism-tests/bugfixes/ctmc-fau-2.sm.props.args new file mode 100644 index 00000000..23ca91b8 --- /dev/null +++ b/prism-tests/bugfixes/ctmc-fau-2.sm.props.args @@ -0,0 +1,3 @@ +-const T=0.2:0.2:1 -transientmethod unif +-const T=0.2:0.2:1 -transientmethod fau + diff --git a/prism/src/explicit/FastAdaptiveUniformisation.java b/prism/src/explicit/FastAdaptiveUniformisation.java index 7f041c01..565b466e 100644 --- a/prism/src/explicit/FastAdaptiveUniformisation.java +++ b/prism/src/explicit/FastAdaptiveUniformisation.java @@ -1175,24 +1175,29 @@ public final class FastAdaptiveUniformisation extends PrismComponent succRates[0] = 1.0; succStates[0] = states.get(state); } else { - int nc = modelGen.getNumChoices(); - succRates = new double[nc]; - succStates = new StateProp[nc]; - for (int i = 0; i < nc; i++) { - int nt = modelGen.getNumTransitions(i); - for (int j = 0; j < nt; j++) { - State succState = modelGen.computeTransitionTarget(i, j); - StateProp succProp = states.get(succState); - if (null == succProp) { - addToModel(succState); - modelGen.exploreState(state); - succProp = states.get(succState); + int ntAll = modelGen.getNumTransitions(); + if (ntAll > 0) { + succRates = new double[ntAll]; + succStates = new StateProp[ntAll]; + + int t = 0; + for (int i = 0, nc = modelGen.getNumChoices(); i < nc; i++) { + for (int j = 0, ntChoice = modelGen.getNumTransitions(i); j < ntChoice; j++) { + State succState = modelGen.computeTransitionTarget(i, j); + StateProp succProp = states.get(succState); + if (null == succProp) { + addToModel(succState); + succProp = states.get(succState); + + // re-explore state, as call to addToModel may have explored succState + modelGen.exploreState(state); + } + succRates[t] = modelGen.getTransitionProbability(i, j); + succStates[t] = succProp; + t++; } - succRates[i] = modelGen.getTransitionProbability(i, j); - succStates[i] = succProp; } - } - if (nc == 0) { + } else { succRates = new double[1]; succStates = new StateProp[1]; succRates[0] = 1.0;