Skip to content

Commit

Permalink
Merge pull request #188 from imitator-model-checker/feat/forall_actions
Browse files Browse the repository at this point in the history 
Forall in action declarations
  • Loading branch information
@himito
himito authored Sep 25, 2024
2 parents da58f52 + 445447a commit 49838cf
Show file tree
Hide file tree
Showing 4 changed files with 59 additions and 20 deletions.
1 change: 1 addition & 0 deletions doc/IMITATOR-user-manual.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2068,6 +2068,7 @@ \section{Model templates}\label{section:templates}
All these constructions are exemplified in the following snippet:

\begin{example}
All these constructions are exemplified in the following snippet:
\begin{IMITATORmodel}
var
id : int;
Expand Down
13 changes: 11 additions & 2 deletions src/lib/ModelParser.mly
View file
Original file line number Diff line number Diff line change
Expand Up @@ -574,13 +574,22 @@ prolog:
/************************************************************/

actions_declarations:
| CT_ACTIONS COLON name_or_array_access_list SEMICOLON { $3 }
| CT_ACTIONS COLON action_declarations_list SEMICOLON { $3 }
/** NOTE: deprecated since 3.4 */
| CT_SYNCLABS COLON name_or_array_access_list SEMICOLON {
| CT_SYNCLABS COLON action_declarations_list SEMICOLON {
print_warning ("The syntax `synclabs` is deprecated since version 3.4; please use `actions` instead.");
$3 }
;

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

action_declarations_list:
| name_or_array_access COMMA action_declarations_list { (Single_action $1) :: $3 }
| name_or_array_access comma_opt { [Single_action $1] }
| forall_common_prefix NAME LSQBRA arithmetic_expression RSQBRA COMMA action_declarations_list { Multiple_actions ($1, $2, $4) :: $7 }
| forall_common_prefix NAME LSQBRA arithmetic_expression RSQBRA comma_opt { [Multiple_actions ($1, $2, $4)] }


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

name_or_array_access_list:
Expand Down
20 changes: 12 additions & 8 deletions src/lib/ParsingStructure.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -279,14 +279,24 @@ type unexpanded_parsed_location = {
unexpanded_transitions : unexpanded_transition list;
}

type forall_index_data = {
forall_index_name : variable_name;
forall_lb : parsed_discrete_arithmetic_expression;
forall_ub : parsed_discrete_arithmetic_expression;
}

type parsed_automaton = automaton_name * action_name list * parsed_location list

type unexpanded_parsed_automaton = automaton_name * name_or_access list * unexpanded_parsed_location list
type action_declaration =
| Single_action of name_or_access
| Multiple_actions of forall_index_data * variable_name * parsed_discrete_arithmetic_expression

type unexpanded_parsed_automaton = automaton_name * action_declaration list * unexpanded_parsed_location list

type parsed_template_definition = {
template_name : template_name;
template_parameters : (variable_name * DiscreteType.template_var_type) list;
template_body : name_or_access list * unexpanded_parsed_location list
template_body : action_declaration list * unexpanded_parsed_location list
}

type parsed_template_arg =
Expand All @@ -299,12 +309,6 @@ type parsed_template_call =
(* name template used parameters passed to template *)
automaton_name * template_name * (parsed_template_arg list)

type forall_index_data = {
forall_index_name : variable_name;
forall_lb : parsed_discrete_arithmetic_expression;
forall_ub : parsed_discrete_arithmetic_expression;
}

type parsed_forall_template_call = {
forall_index_data : forall_index_data;
forall_aut_name : automaton_name;
Expand Down
45 changes: 35 additions & 10 deletions src/lib/Templates.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -237,22 +237,34 @@ let rec instantiate_instructions (param_map : var_map) : parsed_seq_code_bloc ->
| Parsed_local_decl _ ->
raise (Exceptions.InternalError "[instantiate_instructions]: This point of code is unreachable")

let instantiate_action (param_map : var_map) : name_or_access -> name_or_access = fun action ->
let instantiate_name_or_access (param_map : var_map) : name_or_access -> name_or_access = fun action ->
match action with
| Var_name name -> begin
match Hashtbl.find_opt param_map name with
| Some (Arg_name name') -> Var_name name'
| None -> Var_name name
| _ -> failwith "[instantiate_action]: Argument of type action must be a name."
| _ -> failwith "[instantiate_name_or_access]: Argument of type action must be a name."
end
| Var_array_access (arr, index) -> Var_array_access (arr, instantiate_discrete_arithmetic_expression param_map index)

let instantiate_actions (param_map : var_map) : name_or_access list -> name_or_access list =
List.map (instantiate_action param_map)
let instantiate_action_declaration (param_map : var_map) : action_declaration -> action_declaration = function
| Single_action act -> Single_action (instantiate_name_or_access param_map act)
| Multiple_actions (forall_index, arr_name, idx) ->
let prev_binded_value_opt = Hashtbl.find_opt param_map forall_index.forall_index_name in
Hashtbl.remove param_map forall_index.forall_index_name;
let idx' = instantiate_discrete_arithmetic_expression param_map idx in
match prev_binded_value_opt with
| None -> Multiple_actions (forall_index, arr_name, idx')
| Some v ->
Hashtbl.add param_map forall_index.forall_index_name v;
Multiple_actions (forall_index, arr_name, idx')

let instantiate_action_declarations (param_map : var_map) : action_declaration list -> action_declaration list =
List.map (instantiate_action_declaration param_map)

let instantiate_sync (param_map : var_map) : unexpanded_sync -> unexpanded_sync =
function
| UnexpandedSync action -> UnexpandedSync (instantiate_action param_map action)
| UnexpandedSync action -> UnexpandedSync (instantiate_name_or_access param_map action)
| UnexpandedNoSync -> UnexpandedNoSync

let instantiate_transition (param_map : var_map) ((guard, bloc, sync, loc_name) : unexpanded_transition) : unexpanded_transition =
Expand Down Expand Up @@ -280,7 +292,7 @@ let instantiate_automaton (templates : parsed_template_definition list) (parsed_
let param_names = List.map fst template.template_parameters in
let param_map = Hashtbl.of_seq (List.to_seq (List.combine param_names args)) in
let actions, locs = template.template_body in
let instantiated_actions = instantiate_actions param_map actions in
let instantiated_actions = instantiate_action_declarations param_map actions in
(* Instantiate other parameters *)
let instantiated_locs = List.map (instantiate_loc param_map) locs in
(automaton_name, instantiated_actions, instantiated_locs)
Expand Down Expand Up @@ -454,9 +466,22 @@ let expand_loc (g_decls : variable_declarations) (synt_vars : synt_vars_data) (l
transitions = expanded_transitions;
}

let expand_action_declaration (g_decls: variable_declarations) (decl: action_declaration) : variable_name list =
match decl with
| Single_action act -> [expand_name_or_access g_decls act]
| Multiple_actions (forall_index, arr_name, idx) ->
let forall_idx_values = indices_from_forall_index_data g_decls forall_index in
let map_fun idx_value =
let aux_tbl = gen_aux_var_tbl idx_value forall_index in
let idx_instantiated = instantiate_discrete_arithmetic_expression aux_tbl idx in
let idx_concrete = eval_parsed_arithmetic_expr g_decls idx_instantiated in
gen_access_id arr_name (NumConst.to_bounded_int idx_concrete)
in
List.map map_fun forall_idx_values

let expand_synt_arrays_automaton (g_decls : variable_declarations) (synt_vars : synt_vars_data) (automaton : unexpanded_parsed_automaton) : parsed_automaton =
let name, unexpanded_actions, unexpanded_locs = automaton in
let expanded_actions = expand_name_or_access_list g_decls unexpanded_actions in
let expanded_actions = List.concat_map (expand_action_declaration g_decls) unexpanded_actions in
let expanded_locs = List.map (expand_loc g_decls synt_vars) unexpanded_locs in
name, expanded_actions, expanded_locs

Expand Down Expand Up @@ -550,7 +575,7 @@ let expand_model (model : unexpanded_parsed_model) : parsed_model =
init_definition = expanded_init_definition;
}

let instantiate_name_or_access (param_map: var_map) (aut: name_or_access): name_or_access =
let instantiate_name_or_access_properties (param_map: var_map) (aut: name_or_access): name_or_access =
match aut with
| Var_name _ -> aut
| Var_array_access (arr, idx) ->
Expand All @@ -562,10 +587,10 @@ let instantiate_simple_predicate (param_map: var_map) (spred: unexpanded_parsed_
| Unexpanded_Parsed_discrete_boolean_expression expr ->
Unexpanded_Parsed_discrete_boolean_expression (instantiate_discrete_boolean_expression param_map expr)
| Unexpanded_Parsed_loc_predicate (Unexpanded_Parsed_loc_predicate_EQ (aut, loc)) ->
let instantiated_aut = instantiate_name_or_access param_map aut in
let instantiated_aut = instantiate_name_or_access_properties param_map aut in
Unexpanded_Parsed_loc_predicate (Unexpanded_Parsed_loc_predicate_EQ (instantiated_aut, loc))
| Unexpanded_Parsed_loc_predicate (Unexpanded_Parsed_loc_predicate_NEQ (aut, loc)) ->
let instantiated_aut = instantiate_name_or_access param_map aut in
let instantiated_aut = instantiate_name_or_access_properties param_map aut in
Unexpanded_Parsed_loc_predicate (Unexpanded_Parsed_loc_predicate_NEQ (instantiated_aut, loc))
| _ -> spred

Expand Down

0 comments on commit 49838cf

Please sign in to comment.