From c66eecb5cc809a10064ea2aea4f19ee1f0e41f78 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 15 Jul 2009 11:59:17 +0000 Subject: [PATCH] Bug fix in approximate model checking of time-bounded until properties. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1214 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/simpctl.cc | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/prism/src/simulator/simpctl.cc b/prism/src/simulator/simpctl.cc index da625100..29897b7e 100644 --- a/prism/src/simulator/simpctl.cc +++ b/prism/src/simulator/simpctl.cc @@ -349,12 +349,11 @@ void CBoundedUntil::Notify_State(CPathState* last_state, int* current_state) /* * Determines whether the answer is already known for this path formula. This - * will either be if the answer has been proven, or if the answer has not been - * determined but the path is looping. + * will *only* be if the answer has been proven, *not* if the path is looping. */ bool CBoundedUntil::Is_Answer_Known(CLoopDetectionHandler* loop_detection) { - return answer_known || loop_detection->Is_Proven_Looping() || loop_detection->Is_Deadlock(); + return answer_known; } /*