Ecdar / Ecdar/Ecdar-Common

Input language specification

Open
#2 3 comments 3 reactions 0 assignees View on GitHub
documentation
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.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.