IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.
I am not sure if this is expected. If it is not, this can be fixed by replacing fun_parameter_list by fun_parameter_nonempty_list in the last line of the following snippet (lines 309 to 317 of ModelParser.mly):
fun_parameter_list:
| { [] }
| fun_parameter_nonempty_list { $1 }
;
/* Function parameters list (separated by whitespace) */
fun_parameter_nonempty_list:
| NAME COLON var_type_discrete { [(($1, Parsing.symbol_start ()), $3)] }
| fun_parameter_list COMMA NAME COLON var_type_discrete { (($3, Parsing.symbol_start ()), $5) :: $1 }
;
The following syntax does not throw an error:
fn f(,x : int) : int begin end
I am not sure if this is expected. If it is not, this can be fixed by replacing
fun_parameter_list
byfun_parameter_nonempty_list
in the last line of the following snippet (lines 309 to 317 ofModelParser.mly
):