Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Supporting forall and automaton arrays in properties file #186

Merged
merged 9 commits into from
Sep 24, 2024
Merged

Supporting forall and automaton arrays in properties file #186

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
69cf198
allowing accesses in state_predicate
tomaz1502 May 14, 2024
22b0fdd
fischer example with forall in properties
tomaz1502 May 16, 2024
d47aa12
Parsing `forall` in properties
tomaz1502 May 16, 2024
310c0b9
Expanding forall in properties (simple predicates)
tomaz1502 May 16, 2024
faaedc1
Examples with nested forall
tomaz1502 May 16, 2024
cfb0d5d
Supporting nested forall.
tomaz1502 May 16, 2024
570e755
Annotating types in Templates.ml
tomaz1502 May 16, 2024
7085640
Add TODO commentary
tomaz1502 May 16, 2024
9708710
chore: add little comment
himito Sep 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion src/lib/ModelConverter.ml
View file
Open in desktop
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
Open in desktop
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)
75 changes: 75 additions & 0 deletions src/lib/ParsingStructure.mli
View file
Open in desktop
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,22 @@ 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
(* The forall is in this level so we can use it on both sides of `AND` and `OR` *)
| Unexpanded_Parsed_forall_simple_predicate of forall_index_data * unexpanded_parsed_simple_predicate
| Unexpanded_Parsed_forall_state_predicate of forall_index_data * 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 +686,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 +738,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
Open in desktop
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
1 change: 1 addition & 0 deletions src/lib/PropertyLexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,7 @@ rule token = parse
| "eventually" { CT_EVENTUALLY }
| "everytime" { CT_EVERYTIME }
| "False" { CT_FALSE }
| "forall" { CT_FORALL }
| "happened" { CT_HAPPENED }
| "has" { CT_HAS }
| "if" { CT_IF }
Expand Down
Loading
Loading