Repository navigation
Input language specification #2
Description
The purpose of this Issue is to specify what the input format for jecdar and Reveaal should be.
jecdar -i path/to/folder [other-options] ["queries" | /path/to/file-with/queries.q ]
Options
-i, --input-folder path/to/folderOrfile Default value: .
-o, --output-folder path/to/folder Default value: .
-s, --save-to-disk
-h, --help
Queries is a list of queries separated by semicolons ";"
The structure of a queries
Examples of usage:
jecdar -inputFolder path/to/components "refinement: (A && B) ≤ Spec; get-component: (D && F) save-as DandF.json"
jecdar -i . myQueries.q
jecdar -i my/path "reachability: (A[0] && A[server] && A[1]) @ init -> A[0].target and A[server].error or A[1].x ≥ 70 "
Grammar for the queries:
Query ::=
'refinement: ' System ≤ System
| 'get-component: ' SaveSystem
| 'bisim-minim: ' SaveSystem
| 'reachability: ' System ' @ ' SystemStateInit ' -> ' SystemState
| 'Uprune: ' SaveSystem
| 'Eprune: ' SaveSystem
| 'Cprune: ' SaveSystem
Queries ::=
Query
| Query ';' Queries
SaveSystem ::=
System
| System 'as' NewComponentName
System ::=
Component
| System '&&' System
| System '||' System
| System '\\' System
| '(' System ')'
SystemStateInit ::=
'init'
| SystemState
SystemState ::=
SystemLocation
| ClockConstraint
| SystemState BinOp SystemState
| '!' SystemState
| '(' SystemState ')'
BinOp ::=
' and '
| ' or '
SystemLocation ::=
Component'.'Location
Component ::=
componentName
| componentName'[' label ']'
Location ::=
locationName
| 'universal'
| 'error'
ClockConstraint ::=
MaybeClockDiff CompOp MaybeClockDiff
MaybeClockDiff ::=
ClockOrConst
| ClockOrConst ' - ' ClockOrConst
| ClockOrConst ' + ' ClockOrConst
ClockOrConst ::=
Component'.'clockName
| constant
CompOp ::=
' < '
| ' ≤ '
| ' > '
| ' ≥ '
| ' == '
The three operators have the following precedence
- '&&'
- '||'
- '\\'
Reacted by Ulrik Nyman and Thorulf Neustrup
Reacted by Ulrik Nyman
Activity
seblund commentedon Jun 2, 2021
It might be worth considering a different token for naming SaveSystems as '=>' could be confused with the refinement operator '<='. Maybe something like '>>' or '->' ?
ulriknyman commentedon Jun 2, 2021
I think I will actually prefer 'save-as' instead.
'>>' is reserved for a weaken operator which is a combination of composition and quotient.
From: https://vbn.aau.dk/ws/portalfiles/portal/65653882/ownSTTT2012.pdf
seblund commentedon Jul 7, 2021
We should consider adding queries to check for consistency and determinism possibly even implementation and specification, so the GUI does not have to implement that logic.
e.g.
Query ::= 'implementation: ' System | 'specification: ' System | 'consistent: ' System | 'deterministic: ' System ....