Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

Variables with $0 not allowed in DEFINITIONS

Description

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

Environment

None

Gliffy Diagrams

Activity

Show:

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.

Fixed

Details

Assignee

Reporter

Priority

Created April 11, 2016 at 5:59 AM
Updated June 27, 2017 at 2:23 PM
Resolved June 27, 2017 at 2:23 PM
Configure