src/sd_syntax.pest

/*******************************************************************************
* Copyright (c) 2020, 2021 CentraleSupelec, CEA - LIST and others.
*
* This program and the accompanying materials
* are made available under the terms of the Eclipse Public License 2.0
* which accompanies this distribution, and is available at
* https://www.eclipse.org/legal/epl-2.0/
*
* SPDX-License-Identifier: EPL-2.0
*
* Contributors:
* Erwan Mahé (CentraleSupelec) - initial API and implementation
*******************************************************************************/


// ***********************************************
// generic label ; used for variables, lifelines, messages, etc
WHITESPACE = _{ " " | "\r\n" | "\n" | "\t" | "\r" }
HIBOU_LABEL = @{ LETTER ~ (LETTER | ASCII_DIGIT | "_")* }
// ***********************************************
LIFELINE_LABEL   = { HIBOU_LABEL }
MESSAGE_LABEL = { HIBOU_LABEL }
VAR_LABEL = { HIBOU_LABEL }
PRM_LABEL = { HIBOU_LABEL }
// ***********************************************
// ***********************************************

// Typing system

// for declaring types of variables
DATA_TYPE_Clock   = { "Clock" }
DATA_TYPE_Bool    = { "Bool" }
DATA_TYPE_Integer = { "Integer" }
DATA_TYPE_Float   = { "Float" }
DATA_TYPE_String  = { "String" }

DATA_TYPE = _{    DATA_TYPE_Clock
			    | DATA_TYPE_Bool
				| DATA_TYPE_Integer
                | DATA_TYPE_Float
                | DATA_TYPE_String
                }

// for declaring variables and refering to them by name

VAR_DECLARATION = { VAR_LABEL ~ ":" ~ DATA_TYPE }

HIBOU_MODEL_VAR_DECL = { "@variable" ~ "{" ~
	VAR_DECLARATION ~ (";" ~ VAR_DECLARATION)*
    ~ "}"}

PRM_DECLARATION = { PRM_LABEL ~ ":" ~ DATA_TYPE }
PR_DECL = _{ DATA_TYPE | PRM_DECLARATION }
MSG_PR_DECL = { "(" ~ PR_DECL ~ ("," ~ PR_DECL )* ~ ")" }
MESSAGE_DECLARATION = { MESSAGE_LABEL ~ MSG_PR_DECL? }
HIBOU_MODEL_MS_DECL = { "@message" ~ "{" ~
	MESSAGE_DECLARATION ~ (";" ~ MESSAGE_DECLARATION)*
    ~ "}"}

HIBOU_MODEL_LF_DECL = { "@lifeline" ~ "{" ~
	LIFELINE_LABEL ~ (";" ~ LIFELINE_LABEL)* ~ "}"}

VAR_INIT = { LIFELINE_LABEL ~ "." ~ VAR_LABEL ~ "=" ~ TD_VALUE_OR_NEW_FRESH }

HIBOU_MODEL_VAR_INIT = { "@init" ~ "{" ~
	VAR_INIT ~ (";" ~ VAR_INIT)*
    ~ "}"}

// ***********************************************

// numbers and basic arithmetics
ARITH_INTEGER = { "0" | (ASCII_NONZERO_DIGIT ~ ASCII_DIGIT*) }
ARITH_FLOAT_decimal = { ASCII_DIGIT* }
ARITH_FLOAT = { ARITH_INTEGER ~ "." ~ ARITH_FLOAT_decimal }

ARITH_NUMBER = _{ ARITH_FLOAT | ARITH_INTEGER }
ARITH_PLUS = { "+" }
ARITH_MINUS = { "-" }
ARITH_MULT = { "*" }
ARITH_DIV = { "/" }

ARITH_EXPR = { ARITH_FACTOR ~ ARITH_ADD_EXPR* }
ARITH_ADD_EXPR = { (ARITH_PLUS|ARITH_MINUS) ~ ARITH_FACTOR }
ARITH_FACTOR = { ARTIH_PRIMARY ~ ARITH_MULT_EXPR* }
ARITH_MULT_EXPR = { (ARITH_MULT|ARITH_DIV) ~ ARTIH_PRIMARY }
ARTIH_PRIMARY = { "(" ~ ARITH_EXPR ~ ")"
				| ARITH_NUMBER
                | MSG_PRM_REF
                | VAR_LABEL
                | ARITH_MINUS ~ ARTIH_PRIMARY }

// booleans and basic logic
LOGIC_FALSE = { "⊥" }
LOGIC_TRUE = { "⊤" }

LOGIC_SYMB_Diff = { "!=" | "≠" }
LOGIC_SYMB_E = { "==" | "=" }
LOGIC_SYMB_G = { ">" }
LOGIC_SYMB_GoE = {">=" | "≥"}
LOGIC_SYMB_L = { "<" }
LOGIC_SYMB_LoE = { "<=" | "≤" }
LOGIC_SYMB_CMP = _{   LOGIC_SYMB_Diff
                    | LOGIC_SYMB_E
					| LOGIC_SYMB_GoE
                    | LOGIC_SYMB_G
                    | LOGIC_SYMB_LoE
                    | LOGIC_SYMB_L
                    }

LOGIC_SYMB_AND = { ("/\\" | "∧" ) }
LOGIC_SYMB_OR = { ("\\/" | "∨" ) }
LOGIC_NOT = { ("¬"|"!") ~ LOGIC_EXPR }
LOGIC_AND = { LOGIC_EXPR ~ (LOGIC_SYMB_AND ~ LOGIC_EXPR)+ }
LOGIC_OR = { LOGIC_EXPR ~ (LOGIC_SYMB_OR ~ LOGIC_EXPR)+ }
LOGIC_CMP = { TD_VALUE ~ LOGIC_SYMB_CMP ~ TD_VALUE }
LOGIC_EXPR = { 	LOGIC_NOT
				| "(" ~ LOGIC_AND ~ ")"
                | "(" ~ LOGIC_OR ~ ")"
                | "(" ~ LOGIC_CMP ~ ")"
                | MSG_PRM_REF
				| VAR_LABEL
                | LOGIC_FALSE
                | LOGIC_TRUE}

// strings
STRING_content = { (!"\"" ~ ANY)* }
STRING = _{ "\"" ~ STRING_content ~ "\"" }

// everything put together for variable terms

MSG_PRM_REF = { "$" ~ (PRM_LABEL|ARITH_INTEGER) }
TD_VALUE = { STRING
			| MSG_PRM_REF
			| VAR_LABEL
            | ARITH_EXPR
            | LOGIC_EXPR
            }

// ***********************************************


// Sequence Diagrams

SD_GUARD = { "[" ~ LOGIC_EXPR ~ (";" ~ LOGIC_EXPR)* ~ "]" }

NEW_FRESH = { "※" | "#" }
TD_VALUE_OR_NEW_FRESH = _{ TD_VALUE | NEW_FRESH }
OPERATION_ASSIGNMENT = { VAR_LABEL ~ ":=" ~ TD_VALUE_OR_NEW_FRESH }
OPERATION_RESET = { "reset " ~ VAR_LABEL }
SD_OPERATION_content = _{ OPERATION_ASSIGNMENT
                          | OPERATION_RESET
                        }

SD_OPERATION = { "{" ~ SD_OPERATION_content ~ (";" ~ SD_OPERATION_content)* ~ "}" }

SD_ACTION_AMBLE = {(SD_OPERATION|SD_GUARD)+}

//

SD_MESSAGE_PARAMETERS = { "(" ~ TD_VALUE_OR_NEW_FRESH ~ ("," ~ TD_VALUE_OR_NEW_FRESH)* ~ ")" }

SD_LIFELINE_ACTION = { SD_ACTION_AMBLE? ~ LIFELINE_LABEL ~ SD_ACTION_AMBLE? }
SD_EMISSION_TARGETS = { "(" ~ SD_LIFELINE_ACTION ~ ("," ~ SD_LIFELINE_ACTION)* ~ ")" }
SD_EMISSION_TARGET = { SD_LIFELINE_ACTION | SD_EMISSION_TARGETS }
SD_ACTION_EMISSION = { SD_LIFELINE_ACTION ~ "--" ~
            MESSAGE_LABEL ~
            SD_MESSAGE_PARAMETERS?
            ~ "->" ~ (SD_EMISSION_TARGET | "|")}

SD_ACTION_RECEPTION = { ("|" ~ "--")? ~ MESSAGE_LABEL ~
            SD_MESSAGE_PARAMETERS?
            ~ "->" ~ SD_LIFELINE_ACTION}

SD_EMPTY_INTERACTION = {"o" | "∅"}

SD_STRICT = {"@strict"}
SD_STRICT_INT = { SD_STRICT ~ "(" ~ SD_INTERACTION ~ ( "," ~ SD_INTERACTION)+ ~ ")" }

SD_SEQ = {"@seq"}
SD_SEQ_INT = { SD_SEQ ~ "(" ~ SD_INTERACTION ~ ( "," ~ SD_INTERACTION)+ ~ ")" }

SD_ALT = {"@alt"}
SD_ALT_INT = { SD_ALT ~ "(" ~ SD_INTERACTION ~ ( "," ~ SD_INTERACTION)+ ~ ")" }

SD_PAR = {"@par"}
SD_PAR_INT = { SD_PAR ~ "(" ~ SD_INTERACTION ~ ( "," ~ SD_INTERACTION)+ ~ ")" }

SD_LOOP_STRICT = {"@loop_strict"}
SD_LOOP_SEQ = {"@loop_seq"}
SD_LOOP_PAR = {"@loop_par"}
SD_LOOP_INT = { (SD_LOOP_STRICT | SD_LOOP_SEQ | SD_LOOP_PAR) ~ "(" ~ SD_INTERACTION ~ ")" }

SD_SCOPE = {"@scope"}
SD_SCOPED_PARAMS = { VAR_LABEL ~ ("," ~ VAR_LABEL)* }
SD_SCOPE_INT = { SD_SCOPE ~ "{" ~ SD_SCOPED_PARAMS ~ "}" ~ "(" ~ SD_INTERACTION ~ ")" }

SD_INTERACTION = { SD_EMPTY_INTERACTION
		| SD_ACTION_RECEPTION
        | SD_ACTION_EMISSION
        | SD_STRICT_INT
        | SD_SEQ_INT
        | SD_ALT_INT
        | SD_PAR_INT
        | SD_LOOP_INT
        | SD_SCOPE_INT
        }

// ***********************************************
// ***********************************************
// ***********************************************
// ***** hibou options
GRAPHIC_LOGGER_KIND_png = { "png" }
GRAPHIC_LOGGER_KIND_svg = { "svg" }
OPTION_GRAPHIC_LOGGER = { "graphic" ~ ( "=" ~ (GRAPHIC_LOGGER_KIND_png|GRAPHIC_LOGGER_KIND_svg) )? }
OPTION_LOGGER_KIND = _{ OPTION_GRAPHIC_LOGGER }
OPTION_LOGGER_DECL = { "loggers" ~ "=" ~ "[" ~ OPTION_LOGGER_KIND ~ ("," ~ OPTION_LOGGER_KIND)* ~ "]" }
// ***********************************************
OPTION_STRATEGY_BFS = { "BFS" }
OPTION_STRATEGY_DFS = { "DFS" }
OPTION_STRATEGY_KIND = _{ OPTION_STRATEGY_BFS | OPTION_STRATEGY_DFS }
OPTION_STRATEGY_DECL = { "strategy" ~ "=" ~ OPTION_STRATEGY_KIND }
// ***********************************************
// ***********************************************
OPTION_PREFILTER_MAX_DEPTH = { "max_depth" ~ "=" ~ ARITH_INTEGER }
OPTION_PREFILTER_MAX_LOOP_DEPTH = { "max_loop_depth" ~ "=" ~ ARITH_INTEGER }
OPTION_PREFILTER_MAX_NODE_NUMBER = { "max_node_number" ~ "=" ~ ARITH_INTEGER }
OPTION_PREFILTER = _{ OPTION_PREFILTER_MAX_DEPTH | OPTION_PREFILTER_MAX_LOOP_DEPTH | OPTION_PREFILTER_MAX_NODE_NUMBER }
OPTION_PREFILTERS_DECL = { "pre_filters" ~ "=" ~ "[" ~ OPTION_PREFILTER ~ ("," ~ OPTION_PREFILTER)* ~ "]" }
// ***********************************************
OPTION_PRIORITTY_emission = { "emission" }
OPTION_PRIORITTY_reception = { "reception" }
OPTION_PRIORITY_loop = { "loop" }
OPTION_PRIORITY_KIND = _{ OPTION_PRIORITTY_emission | OPTION_PRIORITTY_reception | OPTION_PRIORITY_loop }
OPTION_PRIORITY_LEVEL = { ARITH_INTEGER | ("-" ~ ARITH_INTEGER ) }
OPTION_PRIORITY = { OPTION_PRIORITY_KIND ~ "=" ~ OPTION_PRIORITY_LEVEL }
OPTION_PRIORITIES_DECL = { "frontier_priorities" ~ "=" ~ "[" ~ OPTION_PRIORITY ~ ("," ~ OPTION_PRIORITY)* ~ "]" }
// ***********************************************
OPTION_TEMPORALITY_TIMED = { "temporality" ~ "=" ~ "timed" }
OPTION_TEMPORALITY_UNTIMED = { "temporality" ~ "=" ~ "untimed" }
OPTION_TEMPORALITY = _{ OPTION_TEMPORALITY_TIMED | OPTION_TEMPORALITY_UNTIMED }
// ***********************************************
GENERAL_OPTION_DECL  = _{ OPTION_TEMPORALITY | OPTION_LOGGER_DECL | OPTION_STRATEGY_DECL | OPTION_PREFILTERS_DECL | OPTION_PRIORITIES_DECL }
// ***********************************************
EXPLORE_OPTION_DECL = _{ GENERAL_OPTION_DECL }
EXPLORE_OPTION_SECTION = { "@explore_option" ~ "{" ~
                               	EXPLORE_OPTION_DECL ~ (";" ~ EXPLORE_OPTION_DECL)*
                                   ~ "}"}
// ***********************************************
OPTION_GOAL_pass = { "Pass" }
OPTION_GOAL_weakpass = { "WeakPass" }
OPTION_GOAL_KIND = _{ OPTION_GOAL_pass | OPTION_GOAL_weakpass }
OPTION_GOAL_DECL = { "goal" ~ "=" ~ OPTION_GOAL_KIND }
// ***********************************************
ANALYZE_OPTION_DECL = _{ GENERAL_OPTION_DECL | OPTION_GOAL_DECL }
ANALYZE_OPTION_SECTION =  { "@analyze_option" ~ "{" ~
                               	ANALYZE_OPTION_DECL ~ (";" ~ ANALYZE_OPTION_DECL)*
                                   ~ "}"}
// ***********************************************
// ***********************************************
// setup & .hsf file

SETUP_SECTION = _{ EXPLORE_OPTION_SECTION | ANALYZE_OPTION_SECTION | HIBOU_MODEL_MS_DECL | HIBOU_MODEL_LF_DECL | HIBOU_MODEL_VAR_DECL | HIBOU_MODEL_VAR_INIT }
HIBOU_MODEL_SETUP = { SETUP_SECTION* }
HSF_PEST_FILE = { SOI ~
		HIBOU_MODEL_SETUP ~ SD_INTERACTION ~
        EOI }

// ***********************************************
// ***********************************************
// traces & multitraces
TRACE_LIFELINE = { HIBOU_LABEL }
TRACE_MESSAGE = { HIBOU_LABEL }

TRACE_EMISSION_SYMBOL = { "!" }
TRACE_RECEPTION_SYMBOL = { "?" }

TRACE_LOGIC = _{ LOGIC_FALSE | LOGIC_TRUE }

TRACE_ARGUMENT = { STRING | TRACE_LOGIC | ARITH_FLOAT | ARITH_INTEGER }

TRACE_ARGUMENTS = { "(" ~ TRACE_ARGUMENT ~ ("," ~ TRACE_ARGUMENT)* ~ ")" }
TRACE_DELAY = { "[" ~ ARITH_FLOAT ~ "]" }
TRACE_ACTION = { TRACE_DELAY? ~ TRACE_LIFELINE ~ (TRACE_EMISSION_SYMBOL|TRACE_RECEPTION_SYMBOL) ~ TRACE_MESSAGE ~ TRACE_ARGUMENTS? }
// ***********************************************
CANAL_LIFELINES = { TRACE_LIFELINE ~ ("," ~ TRACE_LIFELINE)* }
CANAL_ANY = {"#any"}
CANAL_ALL = {"#all"}
TRACE_CANAL = _{ "[" ~ (CANAL_ANY | CANAL_ALL | CANAL_LIFELINES) ~ "]" }
TRACE = { TRACE_CANAL ~ (TRACE_ACTION ~ ("." ~ TRACE_ACTION)*)? }
// ***********************************************
MULTI_TRACE = { "{" ~ (TRACE ~ (";" ~ TRACE)* )? ~ "}" }
// ***********************************************
HTF_PEST_FILE = { SOI ~ (MULTI_TRACE|TRACE) ~ EOI }
// ***********************************************