From 5c97413d07104697187dc1c295b123eacca62441 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=89tienne=20Andr=C3=A9?= Date: Fri, 26 Jan 2024 16:59:13 +0100 Subject: [PATCH] Add parsing/converting/printing functionalities for AU algorithm --- src/bin/IMITATOR.ml | 7 +++++++ src/lib/AbstractProperty.mli | 5 ++++- src/lib/AlgoAU.ml | 2 +- src/lib/AlgoAU.mli | 2 +- src/lib/AlgorithmOptions.ml | 19 +++++++++++++++++++ src/lib/Graphics.ml | 5 ++++- src/lib/ModelConverter.ml | 14 +++++++++++++- src/lib/ModelPrinter.ml | 3 +++ src/lib/ParsingStructure.mli | 7 +++++-- src/lib/PropertyLexer.mll | 3 ++- src/lib/PropertyParser.mly | 7 +++++-- 11 files changed, 64 insertions(+), 10 deletions(-) diff --git a/src/bin/IMITATOR.ml b/src/bin/IMITATOR.ml index 7669716a..851fc07f 100644 --- a/src/bin/IMITATOR.ml +++ b/src/bin/IMITATOR.ml @@ -791,6 +791,13 @@ match options#imitator_mode with | AF state_predicate -> let myalgo :> AlgoGeneric.algoGeneric = new AlgoAF.algoAF model property options state_predicate in myalgo + (************************************************************) + (* Always until *) + (************************************************************) + | AU (state_predicate_phi, state_predicate_psi) -> + let myalgo :> AlgoGeneric.algoGeneric = new AlgoAU.algoAU model property options state_predicate_phi state_predicate_psi in myalgo + + (*------------------------------------------------------------*) (* Optimized reachability *) diff --git a/src/lib/AbstractProperty.mli b/src/lib/AbstractProperty.mli index 02dd5ef2..a0b37866 100644 --- a/src/lib/AbstractProperty.mli +++ b/src/lib/AbstractProperty.mli @@ -86,7 +86,10 @@ type property = (* Unavoidability *) | AF of state_predicate - + (* Always until *) + | AU of state_predicate * state_predicate + + (*------------------------------------------------------------*) (* Optimized reachability *) (*------------------------------------------------------------*) diff --git a/src/lib/AlgoAU.ml b/src/lib/AlgoAU.ml index 12e03477..b0f98415 100644 --- a/src/lib/AlgoAU.ml +++ b/src/lib/AlgoAU.ml @@ -26,7 +26,7 @@ open AlgoAUgen (* Class definition *) (************************************************************) (************************************************************) -class algoAF (model : AbstractModel.abstract_model) (property : AbstractProperty.abstract_property) (options : Options.imitator_options) (state_predicate_phi : AbstractProperty.state_predicate) (state_predicate_psi : AbstractProperty.state_predicate) = +class algoAU (model : AbstractModel.abstract_model) (property : AbstractProperty.abstract_property) (options : Options.imitator_options) (state_predicate_phi : AbstractProperty.state_predicate) (state_predicate_psi : AbstractProperty.state_predicate) = object (*(self)*) inherit algoAUgen model property options (Some state_predicate_phi) state_predicate_psi (*as super*) diff --git a/src/lib/AlgoAU.mli b/src/lib/AlgoAU.mli index 5e0c55dc..26620cc8 100644 --- a/src/lib/AlgoAU.mli +++ b/src/lib/AlgoAU.mli @@ -21,7 +21,7 @@ open AlgoAUgen (************************************************************) (* Class definition *) (************************************************************) -class algoAF : AbstractModel.abstract_model -> AbstractProperty.abstract_property -> Options.imitator_options -> AbstractProperty.state_predicate -> AbstractProperty.state_predicate -> +class algoAU : AbstractModel.abstract_model -> AbstractProperty.abstract_property -> Options.imitator_options -> AbstractProperty.state_predicate -> AbstractProperty.state_predicate -> object inherit algoAUgen (************************************************************) (* Class variables *) diff --git a/src/lib/AlgorithmOptions.ml b/src/lib/AlgorithmOptions.ml index c540641a..5516b115 100644 --- a/src/lib/AlgorithmOptions.ml +++ b/src/lib/AlgorithmOptions.ml @@ -59,6 +59,10 @@ let default_state_comparison property : AbstractAlgorithm.state_comparison_opera (*** TODO: decide heuristics ***) -> Equality_check + (* Always until *) + | AU _ + (*** TODO: decide heuristics ***) + -> Equality_check (*------------------------------------------------------------*) (* Optimized reachability *) @@ -195,6 +199,12 @@ let is_state_comparison_correct (abstract_property : AbstractProperty.abstract_p (* No inclusion allowed *) -> state_comparison_operator = Equality_check || state_comparison_operator = No_check + (* Always until *) + | AU _ + (*** TODO: decide heuristics ***) + (* No inclusion allowed *) + -> state_comparison_operator = Equality_check || state_comparison_operator = No_check + (*------------------------------------------------------------*) (* Optimized reachability *) (*------------------------------------------------------------*) @@ -339,6 +349,10 @@ let merge_needed property = (*** TODO: decide heuristics ***) -> false + | AU _ + (*** TODO: decide heuristics ***) + -> false + (*------------------------------------------------------------*) (* Optimized reachability *) (*------------------------------------------------------------*) @@ -584,6 +598,8 @@ let supports_witness property = (* Unavoidability *) | AF _ + (* Always until *) + | AU _ -> false (*------------------------------------------------------------*) @@ -780,6 +796,9 @@ let text_of_property property = (* Unavoidability *) | AF _ -> "unavoidability " ^ synthesis_or_witness + (* Always until *) + | AU _ -> "always until " ^ synthesis_or_witness + (*------------------------------------------------------------*) (* Optimized reachability *) (*------------------------------------------------------------*) diff --git a/src/lib/Graphics.ml b/src/lib/Graphics.ml index 29b2dd25..4dba2408 100644 --- a/src/lib/Graphics.ml +++ b/src/lib/Graphics.ml @@ -157,6 +157,7 @@ let get_v0_option = function | AG _ | EU _ | AF _ + | AU _ | EFpmin _ | EFpmax _ | EFtmin _ @@ -1109,7 +1110,9 @@ let dot_of_statespace (model : AbstractModel.abstract_model) (property_option : | Win (state_predicate) -> [state_predicate] - | EU (state_predicate_1, state_predicate_2) -> [state_predicate_1; state_predicate_2] + | EU (state_predicate_1, state_predicate_2) + | AU (state_predicate_1, state_predicate_2) + -> [state_predicate_1; state_predicate_2] | Cycle_through_generalized state_predicate_list -> state_predicate_list diff --git a/src/lib/ModelConverter.ml b/src/lib/ModelConverter.ml index dfcb5908..ee871d33 100644 --- a/src/lib/ModelConverter.ml +++ b/src/lib/ModelConverter.ml @@ -1892,6 +1892,7 @@ let check_property_option (useful_parsing_model_information : useful_parsing_mod (* Until *) | Parsed_EU (parsed_state_predicate_phi, parsed_state_predicate_psi) + | Parsed_AU (parsed_state_predicate_phi, parsed_state_predicate_psi) -> evaluate_and (check_parsed_state_predicate useful_parsing_model_information parsed_state_predicate_phi) @@ -2222,7 +2223,7 @@ let convert_property_option (useful_parsing_model_information : useful_parsing_m , None - (* Until *) + (* Exists until *) | Parsed_EU (parsed_state_predicate_phi, parsed_state_predicate_psi) -> (* Return a property and no observer *) @@ -2240,6 +2241,17 @@ let convert_property_option (useful_parsing_model_information : useful_parsing_m , None + (* Always until *) + | Parsed_AU (parsed_state_predicate_phi, parsed_state_predicate_psi) + -> + (* Return a property and no observer *) + AU + (PropertyConverter.convert_state_predicate useful_parsing_model_information parsed_state_predicate_phi + , + PropertyConverter.convert_state_predicate useful_parsing_model_information parsed_state_predicate_psi) + , + None + (*------------------------------------------------------------*) (* Optimized reachability *) diff --git a/src/lib/ModelPrinter.ml b/src/lib/ModelPrinter.ml index 371df57a..39dbb18b 100644 --- a/src/lib/ModelPrinter.ml +++ b/src/lib/ModelPrinter.ml @@ -1007,6 +1007,9 @@ let string_of_abstract_property model property = (* Unavoidability *) | AF state_predicate -> "AF(" ^ (string_of_state_predicate model state_predicate) ^ ")" + (* Always until *) + | AU (state_predicate_phi, state_predicate_psi) -> "A(" ^ (string_of_state_predicate model state_predicate_phi) ^ ")U(" ^ (string_of_state_predicate model state_predicate_psi) ^ ")" + (*------------------------------------------------------------*) (* Optimized reachability *) (*------------------------------------------------------------*) diff --git a/src/lib/ParsingStructure.mli b/src/lib/ParsingStructure.mli index 8b413f54..bab45125 100644 --- a/src/lib/ParsingStructure.mli +++ b/src/lib/ParsingStructure.mli @@ -388,13 +388,16 @@ type parsed_property_type = (* Global invariant *) | Parsed_AG of parsed_state_predicate - (* Until *) + (* Exists until *) | Parsed_EU of parsed_state_predicate * parsed_state_predicate (* Unavoidability *) | Parsed_AF of parsed_state_predicate - + (* Always until *) + | Parsed_AU of parsed_state_predicate * parsed_state_predicate + + (*------------------------------------------------------------*) (* Optimized reachability *) (*------------------------------------------------------------*) diff --git a/src/lib/PropertyLexer.mll b/src/lib/PropertyLexer.mll index fe04c839..aa7e6582 100644 --- a/src/lib/PropertyLexer.mll +++ b/src/lib/PropertyLexer.mll @@ -45,6 +45,7 @@ rule token = parse | "#synth" { CT_SYNTH } (* Keywords for properties *) + | "A" { CT_A } | "AccCycle" { CT_ACCEPTINGCYCLE } | "AcceptingCycle" { CT_ACCEPTINGCYCLE } | "AccLoop" { CT_ACCEPTINGCYCLE } @@ -52,7 +53,6 @@ rule token = parse | "AF" { CT_AF } | "AG" { CT_AG } | "AGnot" { CT_AGnot } - | "DeadlockFree" { CT_DEADLOCKFREE } | "BCcover" { CT_COVERCARTOGRAPHY } | "BClearn" { CT_BCLEARN } | "BCshuffle" { CT_BCSHUFFLE } @@ -61,6 +61,7 @@ rule token = parse | "BCrandomseq" { CT_BCRANDOMSEQ } | "Cycle" { CT_INFCYCLE } | "CycleThrough" { CT_INFCYCLETHROUGH } + | "DeadlockFree" { CT_DEADLOCKFREE } | "EF" { CT_EF } | "E" { CT_E } | "EFpmax" { CT_EFpmax } diff --git a/src/lib/PropertyParser.mly b/src/lib/PropertyParser.mly index 45f1d85e..faf96d2c 100644 --- a/src/lib/PropertyParser.mly +++ b/src/lib/PropertyParser.mly @@ -53,7 +53,7 @@ let resolve_property l = %token COLON COMMA DOUBLEDOT SEMICOLON SYMBOL_AND SYMBOL_OR %token - CT_ACCEPTING CT_ACCEPTINGCYCLE CT_AF CT_AG CT_AGnot CT_ALWAYS + CT_A CT_ACCEPTING CT_ACCEPTINGCYCLE CT_AF CT_AG CT_AGnot CT_ALWAYS CT_BCBORDER CT_BCLEARN CT_BCRANDOM CT_BCRANDOMSEQ CT_BCSHUFFLE CT_BEFORE CT_COVERCARTOGRAPHY CT_DEADLOCKFREE @@ -145,12 +145,15 @@ property: /* Global invariant */ | CT_AG state_predicate { Parsed_AG $2 } - /* Until */ + /* Exists until */ | CT_E state_predicate CT_U state_predicate { Parsed_EU ($2, $4) } /* Unavoidability */ | CT_AF state_predicate { Parsed_AF $2 } + /* Always until */ + | CT_A state_predicate CT_U state_predicate { Parsed_AU ($2, $4) } + /*------------------------------------------------------------*/ /* Optimized reachability */