Skip to content

Commit

Permalink
allowing accesses in state_predicate
Browse files Browse the repository at this point in the history
  • Loading branch information
@tomaz1502
tomaz1502 committed May 14, 2024
1 parent 71d9b49 commit 3b14509
Show file tree
Hide file tree
Showing 7 changed files with 251 additions and 96 deletions.
3 changes: 2 additions & 1 deletion src/lib/ModelConverter.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2769,9 +2769,10 @@ let convert_property_option (useful_parsing_model_information : useful_parsing_m
(*------------------------------------------------------------*)
(** Convert the parsed model and the parsed property into an abstract model and an abstract property *)
(*------------------------------------------------------------*)
let abstract_structures_of_parsing_structures options (parsed_model : ParsingStructure.unexpanded_parsed_model) (parsed_property_option : ParsingStructure.parsed_property option) : AbstractModel.abstract_model * (AbstractProperty.abstract_property option) =
let abstract_structures_of_parsing_structures options (parsed_model : ParsingStructure.unexpanded_parsed_model) (parsed_property_option : ParsingStructure.unexpanded_parsed_property option) : AbstractModel.abstract_model * (AbstractProperty.abstract_property option) =

(* Instantiate the template calls and expand syntatic variables *)
let parsed_property_option = Option.map (expand_property parsed_model.unexpanded_variable_declarations) parsed_property_option in
let parsed_model = expand_model parsed_model in

print_message Verbose_high ("\n*** Link variables to declarations.");
Expand Down
2 changes: 1 addition & 1 deletion src/lib/ModelConverter.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,4 +34,4 @@ exception InvalidProperty
(* Conversion functions *)
(****************************************************************)
(** Convert the parsed model and the parsed property into an abstract model and an abstract property *)
val abstract_structures_of_parsing_structures : Options.imitator_options -> ParsingStructure.unexpanded_parsed_model -> (ParsingStructure.parsed_property option) -> AbstractModel.abstract_model * (AbstractProperty.abstract_property option)
val abstract_structures_of_parsing_structures : Options.imitator_options -> ParsingStructure.unexpanded_parsed_model -> (ParsingStructure.unexpanded_parsed_property option) -> AbstractModel.abstract_model * (AbstractProperty.abstract_property option)
72 changes: 72 additions & 0 deletions src/lib/ParsingStructure.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -406,6 +406,10 @@ type parsed_loc_predicate =
| Parsed_loc_predicate_EQ of automaton_name * location_name
| Parsed_loc_predicate_NEQ of automaton_name * location_name

type unexpanded_parsed_loc_predicate =
| Unexpanded_Parsed_loc_predicate_EQ of name_or_access * location_name
| Unexpanded_Parsed_loc_predicate_NEQ of name_or_access * location_name


type parsed_simple_predicate =
| Parsed_discrete_boolean_expression of parsed_discrete_boolean_expression
Expand All @@ -414,6 +418,13 @@ type parsed_simple_predicate =
| Parsed_state_predicate_false
| Parsed_state_predicate_accepting

type unexpanded_parsed_simple_predicate =
| Unexpanded_Parsed_discrete_boolean_expression of parsed_discrete_boolean_expression
| Unexpanded_Parsed_loc_predicate of unexpanded_parsed_loc_predicate
| Unexpanded_Parsed_state_predicate_true
| Unexpanded_Parsed_state_predicate_false
| Unexpanded_Parsed_state_predicate_accepting

type parsed_state_predicate_factor =
| Parsed_state_predicate_factor_NOT of parsed_state_predicate_factor
| Parsed_simple_predicate of parsed_simple_predicate
Expand All @@ -427,6 +438,19 @@ and parsed_state_predicate =
| Parsed_state_predicate_OR of parsed_state_predicate * parsed_state_predicate
| Parsed_state_predicate_term of parsed_state_predicate_term

type unexpanded_parsed_state_predicate_factor =
| Unexpanded_Parsed_state_predicate_factor_NOT of unexpanded_parsed_state_predicate_factor
| Unexpanded_Parsed_simple_predicate of unexpanded_parsed_simple_predicate
| Unexpanded_Parsed_state_predicate of unexpanded_parsed_state_predicate

and unexpanded_parsed_state_predicate_term =
| Unexpanded_Parsed_state_predicate_term_AND of unexpanded_parsed_state_predicate_term * unexpanded_parsed_state_predicate_term
| Unexpanded_Parsed_state_predicate_factor of unexpanded_parsed_state_predicate_factor

and unexpanded_parsed_state_predicate =
| Unexpanded_Parsed_state_predicate_OR of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_state_predicate_term of unexpanded_parsed_state_predicate_term


(****************************************************************)
(* Parsed property *)
Expand Down Expand Up @@ -659,6 +683,48 @@ type parsed_property_type =
| Parsed_Win of parsed_state_predicate


type unexpanded_parsed_property_type =
| Unexpanded_Parsed_Valid
| Unexpanded_Parsed_EF of unexpanded_parsed_state_predicate
| Unexpanded_Parsed_AGnot of unexpanded_parsed_state_predicate
| Unexpanded_Parsed_AG of unexpanded_parsed_state_predicate
| Unexpanded_Parsed_EG of unexpanded_parsed_state_predicate
| Unexpanded_Parsed_ER of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_EU of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_EW of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_AF of unexpanded_parsed_state_predicate
| Unexpanded_Parsed_AR of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_AU of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_AW of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_EF_timed of parsed_interval * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_ER_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_EU_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_EW_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_AF_timed of parsed_interval * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_AR_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_AU_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_AW_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
| Unexpanded_Parsed_EFpmin of unexpanded_parsed_state_predicate * variable_name
| Unexpanded_Parsed_EFpmax of unexpanded_parsed_state_predicate * variable_name
| Unexpanded_Parsed_EFtmin of unexpanded_parsed_state_predicate
| Unexpanded_Parsed_Cycle_Through of unexpanded_parsed_state_predicate
| Unexpanded_Parsed_Cycle_Through_generalized of unexpanded_parsed_state_predicate list
| Unexpanded_Parsed_NZ_Cycle
| Unexpanded_Parsed_Deadlock_Freeness
| Unexpanded_Parsed_IM of parsed_pval
| Unexpanded_Parsed_ConvexIM of parsed_pval
| Unexpanded_Parsed_PRP of unexpanded_parsed_state_predicate * parsed_pval
| Unexpanded_Parsed_IMK of parsed_pval
| Unexpanded_Parsed_IMunion of parsed_pval
| Unexpanded_Parsed_Cover_cartography of parsed_pdomain * NumConst.t
| Unexpanded_Parsed_Learning_cartography of unexpanded_parsed_state_predicate * parsed_pdomain * NumConst.t
| Unexpanded_Parsed_Shuffle_cartography of parsed_pdomain * NumConst.t
| Unexpanded_Parsed_Border_cartography of parsed_pdomain * NumConst.t
| Unexpanded_Parsed_Random_cartography of parsed_pdomain * int * NumConst.t
| Unexpanded_Parsed_RandomSeq_cartography of parsed_pdomain * int * NumConst.t
| Unexpanded_Parsed_PRPC of unexpanded_parsed_state_predicate * parsed_pdomain * NumConst.t
| Unexpanded_Parsed_pattern of parsed_pattern
| Unexpanded_Parsed_Win of unexpanded_parsed_state_predicate

type parsed_property = {
(* Emptiness or synthesis *)
Expand All @@ -669,6 +735,12 @@ type parsed_property = {
projection : parsed_projection;
}

type unexpanded_parsed_property = {
unexpanded_synthesis_type : parsed_synthesis_type;
unexpanded_property : unexpanded_parsed_property_type;
unexpanded_projection : parsed_projection;
}

type declarations_info = {
clock_names : variable_name list;
parameter_names : variable_name list;
Expand Down
2 changes: 1 addition & 1 deletion src/lib/ParsingUtility.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,7 @@ let compile_model_and_property (options : Options.imitator_options) =
print_message Verbose_low ("Parsing property file `" ^ property_file_name ^ "`…");

(* Parsing the property *)
let parsed_property : ParsingStructure.parsed_property = parser_lexer_from_file Property options PropertyParser.main PropertyLexer.token property_file_name in
let parsed_property : ParsingStructure.unexpanded_parsed_property = parser_lexer_from_file Property options PropertyParser.main PropertyLexer.token property_file_name in

(* Statistics *)
parsing_counter#stop;
Expand Down
Loading

0 comments on commit 3b14509

Please sign in to comment.