From f578bbb89338c66bd34dcc95c2f1662149bcc3df Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 4 Oct 2011 20:21:15 +0000 Subject: [PATCH] Approximate model checking ignores "max path length" setting when verifying time-bounded properties. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3855 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/SimulatorEngine.java | 23 +++++++++++++++---- prism/src/simulator/sampler/Sampler.java | 11 +++++++++ .../sampler/SamplerBoundedUntilCont.java | 7 ++++++ .../sampler/SamplerBoundedUntilDisc.java | 7 ++++++ prism/src/simulator/sampler/SamplerNext.java | 7 ++++++ .../sampler/SamplerRewardCumulCont.java | 7 ++++++ .../sampler/SamplerRewardCumulDisc.java | 7 ++++++ .../sampler/SamplerRewardInstCont.java | 7 ++++++ .../sampler/SamplerRewardInstDisc.java | 7 ++++++ 9 files changed, 78 insertions(+), 5 deletions(-) diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index edf99911..af1ceba0 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -29,6 +29,8 @@ package simulator; import java.util.*; import java.io.*; +import javax.swing.plaf.basic.BasicInternalFrameTitlePane.MaximizeAction; + import simulator.method.*; import simulator.sampler.*; import parser.*; @@ -1481,6 +1483,7 @@ public class SimulatorEngine boolean deadlocksFound = false; boolean allDone = false; boolean allKnown = false; + boolean someUnknownButBounded = false; boolean shouldStopSampling = false; // Path stats double avgPathLength = 0; @@ -1526,18 +1529,28 @@ public class SimulatorEngine // Start the new path for this iteration (sample) initialisePath(initialState); - // Generate a path, up to at most maxPathLength steps - for (i = 0; i < maxPathLength; i++) { - // See if all samplers have established a value; if so, stop. + // Generate a path + allKnown = false; + someUnknownButBounded = false; + i = 0; + while ((!allKnown && i < maxPathLength) || someUnknownButBounded) { + // Check status of samplers allKnown = true; + someUnknownButBounded = false; for (Sampler sampler : propertySamplers) { - if (!sampler.isCurrentValueKnown()) + if (!sampler.isCurrentValueKnown()) { allKnown = false; + if (sampler.needsBoundedNumSteps()) + someUnknownButBounded = true; + } } - if (allKnown) + // Stop when all answers are known or we have reached max path length + // (but don't stop yet if there are "bounded" samplers with unkown values) + if ((allKnown || i >= maxPathLength) && !someUnknownButBounded) break; // Make a random transition automaticTransition(); + i++; } // TODO: Detect deadlocks so we can report a warning diff --git a/prism/src/simulator/sampler/Sampler.java b/prism/src/simulator/sampler/Sampler.java index 64843498..dada3a57 100644 --- a/prism/src/simulator/sampler/Sampler.java +++ b/prism/src/simulator/sampler/Sampler.java @@ -52,6 +52,17 @@ public abstract class Sampler return valueKnown; } + /** + * Does this sampler only require a bounded number of path steps? + * i.e. is it safe to keep sampling beyond the maximum path length + * even if this sampler does not know its value yet? + * Conservatively, we assume "no"; override if required. + */ + public boolean needsBoundedNumSteps() + { + return false; + } + /** * Reset the current value of the sampler and whether it is known or not. */ diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java index 6b8cbd83..850f1c30 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilCont.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilCont.java @@ -140,4 +140,11 @@ public class SamplerBoundedUntilCont extends SamplerBoolean return valueKnown; } + + @Override + public boolean needsBoundedNumSteps() + { + // Always bounded (although we don't know the exact num steps, just the time bound) + return true; + } } diff --git a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java index 28ce68eb..ad44f8b5 100644 --- a/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java +++ b/prism/src/simulator/sampler/SamplerBoundedUntilDisc.java @@ -97,4 +97,11 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean return valueKnown; } + + @Override + public boolean needsBoundedNumSteps() + { + // Always bounded + return true; + } } diff --git a/prism/src/simulator/sampler/SamplerNext.java b/prism/src/simulator/sampler/SamplerNext.java index 9da635f6..753ca6f0 100644 --- a/prism/src/simulator/sampler/SamplerNext.java +++ b/prism/src/simulator/sampler/SamplerNext.java @@ -68,4 +68,11 @@ public class SamplerNext extends SamplerBoolean return valueKnown; } + + @Override + public boolean needsBoundedNumSteps() + { + // Always bounded + return true; + } } diff --git a/prism/src/simulator/sampler/SamplerRewardCumulCont.java b/prism/src/simulator/sampler/SamplerRewardCumulCont.java index dc657660..6dfa6c2d 100644 --- a/prism/src/simulator/sampler/SamplerRewardCumulCont.java +++ b/prism/src/simulator/sampler/SamplerRewardCumulCont.java @@ -81,4 +81,11 @@ public class SamplerRewardCumulCont extends SamplerDouble return valueKnown; } + + @Override + public boolean needsBoundedNumSteps() + { + // Always bounded (although we don't know the exact num steps, just the time bound) + return true; + } } diff --git a/prism/src/simulator/sampler/SamplerRewardCumulDisc.java b/prism/src/simulator/sampler/SamplerRewardCumulDisc.java index f74957a2..e2f90da8 100644 --- a/prism/src/simulator/sampler/SamplerRewardCumulDisc.java +++ b/prism/src/simulator/sampler/SamplerRewardCumulDisc.java @@ -69,4 +69,11 @@ public class SamplerRewardCumulDisc extends SamplerDouble return valueKnown; } + + @Override + public boolean needsBoundedNumSteps() + { + // Always bounded + return true; + } } diff --git a/prism/src/simulator/sampler/SamplerRewardInstCont.java b/prism/src/simulator/sampler/SamplerRewardInstCont.java index 8f2c4aae..53e465cb 100644 --- a/prism/src/simulator/sampler/SamplerRewardInstCont.java +++ b/prism/src/simulator/sampler/SamplerRewardInstCont.java @@ -77,4 +77,11 @@ public class SamplerRewardInstCont extends SamplerDouble return valueKnown; } + + @Override + public boolean needsBoundedNumSteps() + { + // Always bounded (although we don't know the exact num steps, just the time bound) + return true; + } } diff --git a/prism/src/simulator/sampler/SamplerRewardInstDisc.java b/prism/src/simulator/sampler/SamplerRewardInstDisc.java index 9a4b4395..8d22616f 100644 --- a/prism/src/simulator/sampler/SamplerRewardInstDisc.java +++ b/prism/src/simulator/sampler/SamplerRewardInstDisc.java @@ -69,4 +69,11 @@ public class SamplerRewardInstDisc extends SamplerDouble return valueKnown; } + + @Override + public boolean needsBoundedNumSteps() + { + // Always bounded + return true; + } }