From 5ed762171f743ced2d9272073c8ccfade3e365f3 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 25 Jul 2018 21:01:58 +0200 Subject: [PATCH] prism-tests: unsupported CTL with step bounds test cases Tweak the result strings for the CTL with step bounds cases (currently computation is not supported with any engine). Previously, an error was expected, but the properties are not actually erroneous. Additonally, the error message was not uniform between the different engines, leading to spurious failures against the exact engine. --- .../functionality/verify/ctl/ctl.prism.props | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/prism-tests/functionality/verify/ctl/ctl.prism.props b/prism-tests/functionality/verify/ctl/ctl.prism.props index c06e0018..ea854030 100644 --- a/prism-tests/functionality/verify/ctl/ctl.prism.props +++ b/prism-tests/functionality/verify/ctl/ctl.prism.props @@ -104,13 +104,16 @@ A [ G E [ X E [X A [ G s=7 ] ] ] ] // RESULT: true A [ G E [ X E [X E [ X A [ G s=7 ] ] ] ] ] -// RESULT: Error:bounded CTL operators is not supported + +// computation of bounded temporal operators for +// CTL path formulas currently unsupported +// RESULT: ? E [ F<3 A [ G s=7 ] ] -// RESULT: Error:bounded CTL operators is not supported +// RESULT: ? E [ G<3 s=0 ] -// RESULT: Error:bounded CTL operators is not supported +// RESULT: ? E [ s=0 U<3 s=1 ] -// RESULT: Error:bounded CTL operators is not supported +// RESULT: ? E [ s=0 R<3 s=1 ] -// RESULT: Error:bounded CTL operators is not supported +// RESULT: ? E [ s=0 W<3 s=1 ]