Variables with $0 not allowed in DEFINITIONS
Description
Environment
Gliffy Diagrams
Activity
Michael Leuschel June 27, 2017 at 2:23 PM
The issue seems fixed. Test 1671 runs successfully.
Jenkins Build Server April 29, 2016 at 4:26 PM
SUCCESS: Integrated in Jenkins build ProB_Tests_Linux64_No_Parallel #22 (See http://cobra.cs.uni-duesseldorf.de/jenkins/job/ProB_Tests_Linux64_No_Parallel/22/)
add test for https://probjira.atlassian.net/browse/PARSERLIB-47#icft=PARSERLIB-47 (leuschel: rev 3c76c1bcbfe3bd0db08aafe172e785f3696e7ac2)
add testcase for https://probjira.atlassian.net/browse/PARSERLIB-47#icft=PARSERLIB-47 (error case) (leuschel: rev e213922c1a2a344ef4d7317479b26bbfcf9d81a7)
Jenkins Build Server April 14, 2016 at 8:46 AM
SUCCESS: Integrated in Jenkins build ProB_Tests_Linux64_On_Commit #2707 (See http://cobra.cs.uni-duesseldorf.de/jenkins/job/ProB_Tests_Linux64_On_Commit/2707/)
add test for https://probjira.atlassian.net/browse/PARSERLIB-47#icft=PARSERLIB-47 (leuschel: rev 3c76c1bcbfe3bd0db08aafe172e785f3696e7ac2)
add testcase for https://probjira.atlassian.net/browse/PARSERLIB-47#icft=PARSERLIB-47 (error case) (leuschel: rev e213922c1a2a344ef4d7317479b26bbfcf9d81a7)
Jenkins Build Server April 13, 2016 at 6:25 PM
SUCCESS: Integrated in Jenkins build ProB_Tests_SMT_Solvers #494 (See http://cobra.cs.uni-duesseldorf.de/jenkins/job/ProB_Tests_SMT_Solvers/494/)
add test for https://probjira.atlassian.net/browse/PARSERLIB-47#icft=PARSERLIB-47 (leuschel: rev 3c76c1bcbfe3bd0db08aafe172e785f3696e7ac2)
add testcase for https://probjira.atlassian.net/browse/PARSERLIB-47#icft=PARSERLIB-47 (error case) (leuschel: rev e213922c1a2a344ef4d7317479b26bbfcf9d81a7)
Michael Leuschel April 13, 2016 at 12:58 PM
The parser has been updated.
Test 1671 has been added.
Incorrect usage is currently reported as identifier not found error message.
The parser does not seem to allow $0 - Variables inside Definitions. Here is an example:
MACHINE AssignByPredicateWithDEF DEFINITIONS lt == xx<xx$0+10 VARIABLES xx INVARIANT xx:NATURAL INITIALISATION xx:=0 OPERATIONS Inc = PRE xx<1000 THEN xx : (xx>xx$0 & lt) END; r <-- Get = BEGIN r:=xx END END
Here the resulting error message:
! An error occurred ! ! source(parse_error) ! construct xx$0 only allowed in become-such-substitutions ! Line: 2 Column: 21 in file: /Users/leuschel/git_root/prob_examples/public_examples/B/FeatureChecks/AssignByPredicateWithDEF.mch