From 481c16f0892c79bfe034b7e7fd02baec97cb146e Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Wed, 1 Mar 2023 15:24:22 +0100 Subject: [PATCH 1/4] Update failures to encompass the different ways that queries can fail --- query.proto | 115 +++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 86 insertions(+), 29 deletions(-) diff --git a/query.proto b/query.proto index 215e8d8..78699fb 100644 --- a/query.proto +++ b/query.proto @@ -26,10 +26,27 @@ message QueryRequest { Settings settings = 6; } -message FailureContext { - string system = 1; - State state = 2; - string action = 3; +message StateAction { + State state = 1; + string action = 2; +} + +enum NoInitialState { + NO_INITIAL_STATE = 0; +} + +message ActionFailure { + enum Relation { + NOT_SUBSET = 0; + NOT_DISJOINT = 1; + } + message ActionSet { + string system = 1; + repeated string actions = 2; + bool is_input = 3; + } + Relation failure = 2; + repeated ActionSet action_sets = 3; } message QueryResponse { @@ -38,55 +55,96 @@ message QueryResponse { message ComponentResult { Component component = 1; } message RefinementFailure { - FailureContext context = 1; - ConsistencyFailure consistency = 4; + string system = 1; + + message RefinementStateFailure { + enum Unmatched { + DELAY = 0; + ACTION = 1; + } + Unmatched unmatched = 1; + StateAction state = 2; + } + + oneof failure { + // The refinement failed for an action in a specific state + RefinementStateFailure refinement_state = 2; + // The refinement failed because this system was empty + string empty_system = 3; + // The refinement failed because the initial state was empty + NoInitialState no_initial_state = 4; + // The refinement failed because a child was inconsistent + ConsistencyFailure inconsistent_child = 5; + // The refinement failed because the actions mismatched + ActionFailure action_mismatch = 6; + } } message ConsistencyFailure { - FailureContext context = 1; - DeterminismFailure determinism = 5; + string system = 1; + oneof failure { + // The consistency check failed because the initial state was empty + NoInitialState no_initial_state = 2; + // The consistency check failed because this state was not consistent + State failure_state = 3; + // The consistency check failed because the system is not deterministic + DeterminismFailure determinism = 4; + } } + message DeterminismFailure { - FailureContext context = 1; + string system = 1; + // The determinism check failed in this state for this action + StateAction failure_state = 2; } + message ImplementationFailure { - FailureContext context = 1; - ConsistencyFailure consistency = 5; + string system = 1; + oneof failure { + // The determinism check failed in this state for this action + StateAction failure_state = 2; + // The implementation check failed because the system was not consistent + ConsistencyFailure consistency = 3; + } } + message ModelFailure { string system = 1; - message ActionFailure { - enum Relation { - NOT_SUBSET = 1; - NOT_DISJOINT = 2; - } - message ActionSet { - string system = 1; - repeated string actions = 2; - } - Relation failure = 2; - repeated ActionSet action_sets = 3; - } oneof failure { - ActionFailure action = 2; - ConsistencyFailure consistency = 3; + // The check failed because the actions mismatched + ActionFailure action_mismatch = 2; + // The check failed because a conjunction was not consistent + ConsistencyFailure inconsistent_conjunction = 3; + // Some other model failure + string other = 4; } } + message ReachabilityFailure { - + enum Failure { + UNREACHABLE = 0; + } + + Failure failure = 1; } message ReachabilityPath { - repeated Path component_paths = 4; + Path path = 4; } + message Success { } + message Error { string error = 1; } + message ParsingError { + string error = 1; + } + oneof result { Component component = 2; ConsistencyFailure consistency = 3; @@ -96,10 +154,10 @@ message QueryResponse { RefinementFailure refinement = 7; ReachabilityPath reachability_path = 8; + ParsingError parsing_error = 98; ModelFailure model = 99; Success success = 100; Error error = 101; - } message Information { @@ -132,4 +190,3 @@ message SimulationInfo { string component_composition = 2; // example: A || B || A ComponentsInfo components_info = 3; } - From a6d842fdf9e3d8a67ec3c0a6ac161759180bd7aa Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Wed, 1 Mar 2023 15:27:12 +0100 Subject: [PATCH 2/4] Change location tuples to a tree structure to support simulation of quotient (Universal and Error in quotient require it) --- objects.proto | 28 ++++++++++++++++++++++++---- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/objects.proto b/objects.proto index 55f96b3..ce0f54a 100644 --- a/objects.proto +++ b/objects.proto @@ -53,17 +53,37 @@ message Federation { Disjunction disjunction = 1; } -message Location { + +// Should only be used when quotient adds new locations to the tree +enum SpecialLocation { + UNIVERSAL = 0; + ERROR = 1; +} + +// A specific location in a specific component +message LeafLocation { string id = 1; SpecificComponent specific_component = 2; } -message LocationTuple { - repeated Location locations = 1; +// A combination/pair of locations +message BranchLocation { + LocationTree left = 1; + LocationTree right = 2; + // Could include composition type too? (e.g. Conjunction, Composition, Quotient, Refinement) +} + +// A binary tree describing a location in a system. It has to be a tree to support the special locations from quotients +message LocationTree { + oneof node_type { + LeafLocation leaf_location = 1; + BranchLocation branch_location = 2; + SpecialLocation special_location = 3; + } } message State { - LocationTuple location_tuple = 1; + LocationTree location_tuple = 1; Federation federation = 2; } From 7684645445e77c3af1ff2a95ae1b0e87d6b87ff3 Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Fri, 3 Mar 2023 15:54:01 +0100 Subject: [PATCH 3/4] Add destination state to all Decision structs --- objects.proto | 2 ++ 1 file changed, 2 insertions(+) diff --git a/objects.proto b/objects.proto index ce0f54a..a35a0c0 100644 --- a/objects.proto +++ b/objects.proto @@ -98,6 +98,8 @@ message Decision { string action = 2; // Only for GUI purposes repeated Edge edges = 3; + // The state that is reached if this decision is taken. Only for GUI purposes. + State destination = 4; } message Path { From 2a1dbd3a7afb7dd52f5beacbe190aaff44a77445 Mon Sep 17 00:00:00 2001 From: Sebastian Lund Date: Fri, 10 Mar 2023 14:04:17 +0100 Subject: [PATCH 4/4] Rename LocationBranch and SpecificComponent to better names --- objects.proto | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/objects.proto b/objects.proto index a35a0c0..07787ed 100644 --- a/objects.proto +++ b/objects.proto @@ -8,14 +8,14 @@ option java_outer_classname = "ObjectProtos"; import "component.proto"; -message SpecificComponent { +message ComponentInstance { string component_name = 1; uint32 component_index = 2; } message Clock { message ComponentClock { - SpecificComponent specific_component = 1; + ComponentInstance component_instance = 1; string clock_name = 2; } message SystemClock { @@ -63,33 +63,39 @@ enum SpecialLocation { // A specific location in a specific component message LeafLocation { string id = 1; - SpecificComponent specific_component = 2; + ComponentInstance component_instance = 2; } -// A combination/pair of locations -message BranchLocation { +// A combination/pair of locations separated by a binary operator (conjunction, composition, quotient, refinement) +message BinaryLocationOperator { LocationTree left = 1; LocationTree right = 2; - // Could include composition type too? (e.g. Conjunction, Composition, Quotient, Refinement) + enum Operator { + CONJUNCTION = 0; + COMPOSITION = 1; + QUOTIENT = 2; + REFINEMENT = 3; + } + Operator operator = 3; } // A binary tree describing a location in a system. It has to be a tree to support the special locations from quotients message LocationTree { oneof node_type { LeafLocation leaf_location = 1; - BranchLocation branch_location = 2; + BinaryLocationOperator binary_location_op = 2; SpecialLocation special_location = 3; } } message State { - LocationTree location_tuple = 1; + LocationTree location_tree = 1; Federation federation = 2; } message Edge { string id = 1; - SpecificComponent specific_component = 2; + ComponentInstance component_instance = 2; } message Decision {