Commit 1361e3f2 authored by Pietro Braghieri's avatar Pietro Braghieri
Browse files

Merge branch '37-align-sde-grammar-to-new-timed-features' into 'master'

Resolve "Align SDE grammar to new timed features"

Closes #37

See merge request ESProjects/SDE!60
parents aaa9ee5a 02a48ed6
@TIME_DOMAIN none
MODULE main
VAR
state : { OK,
failure
};
IVAR
fault_Monitor : boolean;
fault_Command : boolean;
Pedal_Pos : boolean;
CMD_AS : boolean;
DEFINE
Valid := state!=failure;
fault := (fault_Command | fault_Monitor);
-- INIT
-- state = OK
-- TRANS
-- (state = OK & !fault & next(state) = OK & (Pedal_Pos -> CMD_AS)) |
-- (state = OK & fault & next(state) = failure) |
-- (state = failure & next(state) = failure)
-- This is designed to be equivalent to the previous code
ASSIGN
init(state) := OK;
next(state) :=
case
state = OK & !fault : OK;
state = OK & fault : failure;
TRUE : failure;
esac;
TRANS
(state = OK & !fault & next(state) = OK & Pedal_Pos) -> CMD_AS;
@TIME_DOMAIN continuous
MODULE main
VAR
state : { OK,
failure
};
IVAR
fault_Monitor : boolean;
fault_Command : boolean;
Pedal_Pos : boolean;
CMD_AS : boolean;
DEFINE
Valid := state!=failure;
fault := (fault_Command | fault_Monitor);
-- INIT
-- state = OK
-- TRANS
-- (state = OK & !fault & next(state) = OK & (Pedal_Pos -> CMD_AS)) |
-- (state = OK & fault & next(state) = failure) |
-- (state = failure & next(state) = failure)
-- This is designed to be equivalent to the previous code
ASSIGN
init(state) := OK;
next(state) :=
case
state = OK & !fault : OK;
state = OK & fault : failure;
TRUE : failure;
esac;
TRANS
(state = OK & !fault & next(state) = OK & Pedal_Pos) -> CMD_AS;
......@@ -15,9 +15,13 @@ generate smv "http://www.fbk.eu/tools/editor/nusmv/NuSMV"
import "http://www.fbk.eu/tools/editor/basetype/BaseType"
Model hidden(WS, SL_COMMENT):
(modules+=Module)+;
Model:
annotation=TimeAnnotation?
modules+=Module+;
TimeAnnotation:
'@TIME_DOMAIN' value=('none' | 'continuous');
Module:
'MODULE' identifier=ComponentId (LPAREN (moduleParameters+=ModuleParameter (COMMA moduleParameters+=ModuleParameter)*)? RPAREN)? (moduleElements+=ModuleElement)*;
......@@ -292,7 +296,7 @@ Identifier:
{Identifier} value=(ID | EXPONENT_LITERAL | 'self') // trick allowing identifier with shape of exponent (i.e. E12, e+2, e-10)
;
@Override
@Override
SimpleType:
BooleanType |
IntegerType |
......@@ -313,10 +317,10 @@ EventType:
terminal ID:
(ALPHA_CHAR | '_') (ALPHA_CHAR | INT | '_' | '$' | '#' | '-')*;
@Override
@Override
terminal SL_COMMENT:
'--' !('\n' | '\r')* ('\r'? '\n')?;
@Override
@Override
terminal STRING:
'\"' '&' ID (' ' ID)* '\"';
\ No newline at end of file
......@@ -16,16 +16,32 @@ import eu.fbk.tools.editor.nusmv.smv.DefineDeclaration
import eu.fbk.tools.editor.nusmv.smv.FunctionDeclaration
import eu.fbk.tools.editor.nusmv.smv.CaseExpression
import eu.fbk.tools.editor.nusmv.smv.AssignDeclaration
import eu.fbk.tools.editor.nusmv.smv.TimeAnnotation
class NuSMVFormatter extends AbstractFormatter2 {
@Inject extension NuSMVGrammarAccess
def dispatch void format(Model model, extension IFormattableDocument document) {
// TODO: format HiddenRegions around keywords, attributes, cross references, etc.
// TODO: format HiddenRegions around keywords, attributes, cross references, etc.
model.annotation.format
for (module : model.getModules()) {
module.append[newLine].format;
}
if( model.annotation.value !== null ) // trick because call to model.annotation.format seems not working
{
module.surround[newLine].format
}
else
{
module.append[newLine].format
}
}
}
def dispatch void format(TimeAnnotation annotation, extension IFormattableDocument document) {
annotation.append[newLine]
}
def dispatch void format(Module module, extension IFormattableDocument document) {
......
@requires discrete-time
COMPONENT test system
INTERFACE
INPUT PORT electrical_command: boolean;
INPUT PORT pressure_in: boolean;
OUTPUT PORT pressure_out: boolean;
REFINEMENT
SUB sub_sys: SubSystem;
CONNECTION sub_sys.electrical_command:=electrical_command;
CONNECTION sub_sys.pressure_in:=pressure_in;
CONNECTION pressure_out:=sub_sys.pressure_out;
CONNECTION sub_sys.mechanical_command:=false;
CONNECTION sub_sys.phase:=10;
COMPONENT SubSystem
INTERFACE
INPUT PORT electrical_command: boolean;
INPUT PORT mechanical_command: boolean;
INPUT PORT phase:0..10;
INPUT PORT pressure_in: boolean;
OUTPUT PORT pressure_out: boolean;
\ No newline at end of file
@requires hybrid-time
COMPONENT test system
INTERFACE
INPUT PORT electrical_command: boolean;
INPUT PORT pressure_in: boolean;
OUTPUT PORT pressure_out: boolean;
REFINEMENT
SUB sub_sys: SubSystem;
CONNECTION sub_sys.electrical_command:=electrical_command;
CONNECTION sub_sys.pressure_in:=pressure_in;
CONNECTION pressure_out:=sub_sys.pressure_out;
CONNECTION sub_sys.mechanical_command:=false;
CONNECTION sub_sys.phase:=10;
COMPONENT SubSystem
INTERFACE
INPUT PORT electrical_command: boolean;
INPUT PORT mechanical_command: boolean;
INPUT PORT phase:0..10;
INPUT PORT pressure_in: boolean;
OUTPUT PORT pressure_out: boolean;
\ No newline at end of file
@requires timed-domain
COMPONENT test system
INTERFACE
INPUT PORT electrical_command: boolean;
INPUT PORT pressure_in: boolean;
OUTPUT PORT pressure_out: boolean;
REFINEMENT
SUB sub_sys: SubSystem;
CONNECTION sub_sys.electrical_command:=electrical_command;
CONNECTION sub_sys.pressure_in:=pressure_in;
CONNECTION pressure_out:=sub_sys.pressure_out;
CONNECTION sub_sys.mechanical_command:=false;
CONNECTION sub_sys.phase:=10;
COMPONENT SubSystem
INTERFACE
INPUT PORT electrical_command: boolean;
INPUT PORT mechanical_command: boolean;
INPUT PORT phase:0..10;
INPUT PORT pressure_in: boolean;
OUTPUT PORT pressure_out: boolean;
\ No newline at end of file
......@@ -24,7 +24,7 @@ PreprocessorDirective:
'#include' QUOTE value=IncludeFileName QUOTE;
TimeAnnotation:
'@requires' value=('discrete-time' | 'hybrid-time');
'@requires' value=('discrete-time' | 'hybrid-time' | 'timed-domain');
SystemComponent:
(comment='/--' -> '--/')? 'COMPONENT' type=ComponentType? 'system' interface=Interface (refinement=Refinement)?;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment