Input language specification

[ulriknyman]

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. '\\'

[seblund]

It might be worth considering a different token for naming SaveSystems as '=>' could be confused with the refinement operator '<='. Maybe something like '>>' or '->' ?

[ulriknyman]

I think I will actually prefer 'save-as' instead.
'>>' is reserved for a weaken operator which is a combination of composition and quotient.

Definition 6 Weaken >>:
For any two Timed Input/Output Automata specifications A and G we define G >> A as follows:
G >> A ≡ (A||G)\A

From: https://vbn.aau.dk/ws/portalfiles/portal/65653882/ownSTTT2012.pdf

[seblund]

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 ....