Input language specification
- Dominant language
- No language data
- Stars
- 0
- Forks
- 2
- PR merge metrics
- No merged PRs in 30d
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
1. '&&'
2. '||'
3. '\\\\'
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.