From fc57fde9e8204b58638f950ad38a37a68d81a8c8 Mon Sep 17 00:00:00 2001 From: Lasse Date: Mon, 7 Nov 2022 15:51:10 +0100 Subject: [PATCH 1/7] Added collection of action string to Determinism, consistency and refinement query failure. --- .../ecdar_requests/send_query.rs | 26 ++++++++-- src/System/executable_query.rs | 6 +-- src/System/local_consistency.rs | 48 +++++++++++++------ src/System/pruning.rs | 2 +- src/System/refine.rs | 42 ++++++++-------- src/TransitionSystems/common.rs | 4 +- src/TransitionSystems/compiled_component.rs | 4 +- src/TransitionSystems/quotient.rs | 4 +- src/TransitionSystems/transition_system.rs | 2 +- 9 files changed, 84 insertions(+), 54 deletions(-) diff --git a/src/ProtobufServer/ecdar_requests/send_query.rs b/src/ProtobufServer/ecdar_requests/send_query.rs index 81f80c2b..3433a4d7 100644 --- a/src/ProtobufServer/ecdar_requests/send_query.rs +++ b/src/ProtobufServer/ecdar_requests/send_query.rs @@ -153,6 +153,7 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option { reason: "".to_string(), relation: vec![], state: None, + action: "".to_string(), })) } refine::RefinementResult::Failure(failure) => convert_refinement_failure(failure), @@ -173,6 +174,7 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option { success: true, reason: "".to_string(), state: None, + action: "".to_string(), })) } ConsistencyResult::Failure(failure) => match failure { @@ -181,10 +183,11 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option { success: false, reason: failure.to_string(), state: None, + action: "".to_string(), })) } - ConsistencyFailure::NotConsistentFrom(location_id) - | ConsistencyFailure::NotDeterministicFrom(location_id) => { + ConsistencyFailure::NotConsistentFrom(location_id, action) + | ConsistencyFailure::NotDeterministicFrom(location_id, action) => { Some(ProtobufResult::Consistency(ProtobufConsistencyResult { success: false, reason: failure.to_string(), @@ -197,6 +200,7 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option { }), federation: None, }), + action: action.to_string(), })) } }, @@ -207,9 +211,10 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option { success: true, reason: "".to_string(), state: None, + action: "".to_string(), })) } - DeterminismResult::Failure(location_id) => { + DeterminismResult::Failure(location_id, action) => { Some(ProtobufResult::Determinism(ProtobufDeterminismResult { success: false, reason: "Not deterministic From Location".to_string(), @@ -222,6 +227,7 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option { }), federation: None, }), + action: action.to_string(), })) } }, @@ -241,6 +247,7 @@ fn convert_refinement_failure(failure: &RefinementFailure) -> Option Option { + RefinementFailure::ConsistencyFailure(location_id, action) + | RefinementFailure::DeterminismFailure(location_id, action) => { Some(ProtobufResult::Refinement(RefinementResult { success: false, reason: failure.to_string(), @@ -276,6 +284,7 @@ fn convert_refinement_failure(failure: &RefinementFailure) -> Option) -> String { None => "".to_string(), } } + +fn value_in_action(maybe_action: &Option) -> String{ + match maybe_action{ + Some(action) => action.to_string(), + None => "".to_string(), + } +} diff --git a/src/System/executable_query.rs b/src/System/executable_query.rs index 46bcfc4a..e3a22640 100644 --- a/src/System/executable_query.rs +++ b/src/System/executable_query.rs @@ -38,7 +38,7 @@ impl QueryResult { QueryResult::Consistency(ConsistencyResult::Failure(_)) => not_satisfied(query_str), QueryResult::Determinism(DeterminismResult::Success) => satisfied(query_str), - QueryResult::Determinism(DeterminismResult::Failure(_)) => not_satisfied(query_str), + QueryResult::Determinism(DeterminismResult::Failure(_, _)) => not_satisfied(query_str), QueryResult::GetComponent(_) => { println!("{} -- Component succesfully created", query_str) @@ -125,8 +125,8 @@ impl ExecutableQuery for ConsistencyExecutor { let res = match self.recipe.compile(self.dim) { Ok(system) => match system.precheck_sys_rep() { PrecheckResult::Success => QueryResult::Consistency(ConsistencyResult::Success), - PrecheckResult::NotDeterministic(location) => QueryResult::Consistency( - ConsistencyResult::Failure(ConsistencyFailure::NotDeterministicFrom(location)), + PrecheckResult::NotDeterministic(location, action) => QueryResult::Consistency( + ConsistencyResult::Failure(ConsistencyFailure::NotDeterministicFrom(location, action)), ), PrecheckResult::NotConsistent(failure) => { QueryResult::Consistency(ConsistencyResult::Failure(failure)) diff --git a/src/System/local_consistency.rs b/src/System/local_consistency.rs index 841eb324..fb425957 100644 --- a/src/System/local_consistency.rs +++ b/src/System/local_consistency.rs @@ -27,8 +27,8 @@ impl fmt::Display for ConsistencyResult { pub enum ConsistencyFailure { NoInitialLocation, EmptyInitialState, - NotConsistentFrom(LocationID), - NotDeterministicFrom(LocationID), + NotConsistentFrom(LocationID, String), // TODO maybe Option is wrong. + NotDeterministicFrom(LocationID, String), } impl fmt::Display for ConsistencyFailure { @@ -36,11 +36,11 @@ impl fmt::Display for ConsistencyFailure { match self { ConsistencyFailure::NoInitialLocation => write!(f, "No Initial State"), ConsistencyFailure::EmptyInitialState => write!(f, "Empty Initial State"), - ConsistencyFailure::NotConsistentFrom(location) => { - write!(f, "Not Consistent From {}", location) + ConsistencyFailure::NotConsistentFrom(location, action) => { + write!(f, "Not Consistent From {} Failing action {}", location, action) } - ConsistencyFailure::NotDeterministicFrom(location) => { - write!(f, "Not Deterministic From {}", location) + ConsistencyFailure::NotDeterministicFrom(location, action) => { + write!(f, "Not Deterministic From {} Failing action {}", location, action) } } } @@ -50,15 +50,15 @@ impl fmt::Display for ConsistencyFailure { /// Failure includes the [LocationID]. pub enum DeterminismResult { Success, - Failure(LocationID), -} + Failure(LocationID, String), +} impl fmt::Display for DeterminismResult { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { match self { DeterminismResult::Success => write!(f, "Success"), - DeterminismResult::Failure(location) => { - write!(f, "Not Deterministic From {}", location) + DeterminismResult::Failure(location, action) => { + write!(f, "Not Deterministic From {} failing action {}", location, action) } } } @@ -117,18 +117,19 @@ fn is_deterministic_helper( allowed_fed = state.decorated_locations.apply_invariants(allowed_fed); if allowed_fed.has_intersection(&location_fed) { warn!( - "Not deterministic from location {}", - state.get_location().id + "Not deterministic from location {} failing action {}", + state.get_location().id, + action ); - return DeterminismResult::Failure(state.get_location().id.clone()); + return DeterminismResult::Failure(state.get_location().id.clone(), action); } location_fed += allowed_fed; new_state.extrapolate_max_bounds(system); - if let DeterminismResult::Failure(location) = + if let DeterminismResult::Failure(location, action) = is_deterministic_helper(new_state, passed_list, system) { - return DeterminismResult::Failure(location); + return DeterminismResult::Failure(location, action); } } } @@ -157,6 +158,8 @@ pub fn consistency_least_helper( passed_list: &mut Vec, system: &dyn TransitionSystem, ) -> ConsistencyResult { + let mut failing_action = String::new(); + if state.is_contained_in_list(passed_list) { return ConsistencyResult::Success; } @@ -166,6 +169,7 @@ pub fn consistency_least_helper( if state.decorated_locations.is_inconsistent() { return ConsistencyResult::Failure(ConsistencyFailure::NotConsistentFrom( state.get_location().id.clone(), + failing_action, // TODO FIX. )); } @@ -185,6 +189,8 @@ pub fn consistency_least_helper( ); return ConsistencyResult::Failure(failure); } + } else{ + failing_action = input.clone(); } } } @@ -203,12 +209,16 @@ pub fn consistency_least_helper( { return ConsistencyResult::Success; } + } else { + failing_action = output.clone(); } } } + warn!("failing action {}", failing_action); warn!("No saving outputs from {}", state.get_location().id); ConsistencyResult::Failure(ConsistencyFailure::NotConsistentFrom( state.get_location().id.clone(), + failing_action, )) } @@ -218,6 +228,8 @@ fn consistency_fully_helper( passed_list: &mut Vec, system: &dyn TransitionSystem, ) -> ConsistencyResult { + let mut failing_action = String::new(); + if state.is_contained_in_list(passed_list) { return ConsistencyResult::Success; } @@ -236,6 +248,8 @@ fn consistency_fully_helper( { return ConsistencyResult::Failure(failure); } + } else{ + failing_action = input.clone(); } } } @@ -257,9 +271,12 @@ fn consistency_fully_helper( { return ConsistencyResult::Failure(failure); } + } else{ + failing_action = output.clone(); } } } + warn!("failing action {}", failing_action); if output_existed { ConsistencyResult::Success } else { @@ -267,6 +284,7 @@ fn consistency_fully_helper( match last_state.zone_ref().can_delay_indefinitely() { false => ConsistencyResult::Failure(ConsistencyFailure::NotConsistentFrom( last_state.get_location().id.clone(), + failing_action, )), true => ConsistencyResult::Success, } diff --git a/src/System/pruning.rs b/src/System/pruning.rs index 0718d96e..17115e7a 100644 --- a/src/System/pruning.rs +++ b/src/System/pruning.rs @@ -21,7 +21,7 @@ pub fn prune_system(ts: TransitionSystemPtr, dim: ClockIndex) -> TransitionSyste let outputs = ts.get_output_actions(); let comp = combine_components(&ts, PruningStrategy::NoPruning); - if let PrecheckResult::NotDeterministic(_) | PrecheckResult::NotConsistent(_) = + if let PrecheckResult::NotDeterministic(_, _) | PrecheckResult::NotConsistent(_) = ts.precheck_sys_rep() { panic!("Trying to prune transitions system which is not least consistent") diff --git a/src/System/refine.rs b/src/System/refine.rs index 54549a4a..d39d803e 100644 --- a/src/System/refine.rs +++ b/src/System/refine.rs @@ -32,8 +32,8 @@ pub enum RefinementFailure { EmptyImplementation, EmptyTransition2s(StatePair), NotEmptyResult(StatePair), - ConsistencyFailure(Option), - DeterminismFailure(Option), + ConsistencyFailure(Option, Option), + DeterminismFailure(Option, Option), } enum StatePairResult { Valid, @@ -54,10 +54,10 @@ impl fmt::Display for RefinementFailure { RefinementFailure::EmptyImplementation => write!(f, "Empty Implementation"), RefinementFailure::EmptyTransition2s(_) => write!(f, "Empty Transition2s"), RefinementFailure::NotEmptyResult(_) => write!(f, "Not Empty Result on State Pair"), - RefinementFailure::ConsistencyFailure(location) => { - write!(f, "Not Consistent From {}", location.as_ref().unwrap()) + RefinementFailure::ConsistencyFailure(location, action) => { + write!(f, "Not Consistent From {} failing action {}", location.as_ref().unwrap(), action.as_ref().unwrap()) } - RefinementFailure::DeterminismFailure(location) => { + RefinementFailure::DeterminismFailure(location, action ) => { write!(f, "Not Deterministic From {}", location.as_ref().unwrap()) } } @@ -552,46 +552,42 @@ fn prepare_init_state( fn check_preconditions(sys1: &TransitionSystemPtr, sys2: &TransitionSystemPtr) -> RefinementResult { match sys1.precheck_sys_rep() { PrecheckResult::Success => {} - PrecheckResult::NotDeterministic(location) => { + PrecheckResult::NotDeterministic(location, action) => { warn!("Refinement failed - sys1 is not deterministic"); - return RefinementResult::Failure(RefinementFailure::DeterminismFailure(Some( - location, - ))); + return RefinementResult::Failure(RefinementFailure::DeterminismFailure(Some(location), Some(action))); } PrecheckResult::NotConsistent(failure) => { warn!("Refinement failed - sys1 is inconsistent"); match failure { ConsistencyFailure::NoInitialLocation | ConsistencyFailure::EmptyInitialState => { - return RefinementResult::Failure(RefinementFailure::ConsistencyFailure(None)) + return RefinementResult::Failure(RefinementFailure::ConsistencyFailure(None, None)) } - ConsistencyFailure::NotConsistentFrom(location) - | ConsistencyFailure::NotDeterministicFrom(location) => { + ConsistencyFailure::NotConsistentFrom(location, action) + | ConsistencyFailure::NotDeterministicFrom(location, action) => { return RefinementResult::Failure(RefinementFailure::ConsistencyFailure(Some( - location, - ))) + location), Some(action), + )) } } } } match sys2.precheck_sys_rep() { PrecheckResult::Success => {} - PrecheckResult::NotDeterministic(location) => { + PrecheckResult::NotDeterministic(location, action) => { warn!("Refinement failed - sys2 is not deterministic"); - return RefinementResult::Failure(RefinementFailure::DeterminismFailure(Some( - location, - ))); + return RefinementResult::Failure(RefinementFailure::DeterminismFailure(Some(location), Some(action))); } PrecheckResult::NotConsistent(failure) => { warn!("Refinement failed - sys2 is inconsistent"); match failure { ConsistencyFailure::NoInitialLocation | ConsistencyFailure::EmptyInitialState => { - return RefinementResult::Failure(RefinementFailure::ConsistencyFailure(None)) + return RefinementResult::Failure(RefinementFailure::ConsistencyFailure(None, None)) } - ConsistencyFailure::NotConsistentFrom(location) - | ConsistencyFailure::NotDeterministicFrom(location) => { + ConsistencyFailure::NotConsistentFrom(location, action) + | ConsistencyFailure::NotDeterministicFrom(location, action) => { return RefinementResult::Failure(RefinementFailure::ConsistencyFailure(Some( - location, - ))) + location), Some(action), + )) } } } diff --git a/src/TransitionSystems/common.rs b/src/TransitionSystems/common.rs index 7a58e5fa..a91caf25 100644 --- a/src/TransitionSystems/common.rs +++ b/src/TransitionSystems/common.rs @@ -84,9 +84,9 @@ impl TransitionSystem for T { } fn precheck_sys_rep(&self) -> PrecheckResult { - if let DeterminismResult::Failure(location) = self.is_deterministic() { + if let DeterminismResult::Failure(location, action) = self.is_deterministic() { warn!("Not deterministic"); - return PrecheckResult::NotDeterministic(location); + return PrecheckResult::NotDeterministic(location, action); } if let ConsistencyResult::Failure(failure) = self.is_locally_consistent() { diff --git a/src/TransitionSystems/compiled_component.rs b/src/TransitionSystems/compiled_component.rs index d9e2c54b..5e33b457 100644 --- a/src/TransitionSystems/compiled_component.rs +++ b/src/TransitionSystems/compiled_component.rs @@ -171,9 +171,9 @@ impl TransitionSystem for CompiledComponent { } fn precheck_sys_rep(&self) -> PrecheckResult { - if let DeterminismResult::Failure(location) = self.is_deterministic() { + if let DeterminismResult::Failure(location, action) = self.is_deterministic() { warn!("Not deterministic"); - return PrecheckResult::NotDeterministic(location); + return PrecheckResult::NotDeterministic(location, action); } if let ConsistencyResult::Failure(failure) = self.is_locally_consistent() { diff --git a/src/TransitionSystems/quotient.rs b/src/TransitionSystems/quotient.rs index 4ba0a78b..5f4a64e6 100644 --- a/src/TransitionSystems/quotient.rs +++ b/src/TransitionSystems/quotient.rs @@ -383,9 +383,9 @@ impl TransitionSystem for Quotient { } fn precheck_sys_rep(&self) -> PrecheckResult { - if let DeterminismResult::Failure(location) = self.is_deterministic() { + if let DeterminismResult::Failure(location, action) = self.is_deterministic() { warn!("Not deterministic"); - return PrecheckResult::NotDeterministic(location); + return PrecheckResult::NotDeterministic(location, action); } if let ConsistencyResult::Failure(failure) = self.is_locally_consistent() { diff --git a/src/TransitionSystems/transition_system.rs b/src/TransitionSystems/transition_system.rs index 4c069348..dfd87acb 100644 --- a/src/TransitionSystems/transition_system.rs +++ b/src/TransitionSystems/transition_system.rs @@ -13,7 +13,7 @@ pub type TransitionSystemPtr = Box; /// Precheck can fail because of either consistency or determinism. pub enum PrecheckResult { Success, - NotDeterministic(LocationID), + NotDeterministic(LocationID, String), NotConsistent(ConsistencyFailure), } From 2672847c9738e766d5567e55e99a047c32aef6f3 Mon Sep 17 00:00:00 2001 From: Lasse Date: Mon, 7 Nov 2022 22:24:24 +0100 Subject: [PATCH 2/7] cargo formatting and removal of a few warn. --- .../ecdar_requests/send_query.rs | 4 +- src/System/executable_query.rs | 8 ++-- src/System/local_consistency.rs | 30 ++++++++----- src/System/refine.rs | 44 ++++++++++++++----- 4 files changed, 60 insertions(+), 26 deletions(-) diff --git a/src/ProtobufServer/ecdar_requests/send_query.rs b/src/ProtobufServer/ecdar_requests/send_query.rs index 3433a4d7..3c5f6c66 100644 --- a/src/ProtobufServer/ecdar_requests/send_query.rs +++ b/src/ProtobufServer/ecdar_requests/send_query.rs @@ -342,8 +342,8 @@ fn value_in_location(maybe_location: &Option) -> String { } } -fn value_in_action(maybe_action: &Option) -> String{ - match maybe_action{ +fn value_in_action(maybe_action: &Option) -> String { + match maybe_action { Some(action) => action.to_string(), None => "".to_string(), } diff --git a/src/System/executable_query.rs b/src/System/executable_query.rs index e3a22640..33c680aa 100644 --- a/src/System/executable_query.rs +++ b/src/System/executable_query.rs @@ -125,9 +125,11 @@ impl ExecutableQuery for ConsistencyExecutor { let res = match self.recipe.compile(self.dim) { Ok(system) => match system.precheck_sys_rep() { PrecheckResult::Success => QueryResult::Consistency(ConsistencyResult::Success), - PrecheckResult::NotDeterministic(location, action) => QueryResult::Consistency( - ConsistencyResult::Failure(ConsistencyFailure::NotDeterministicFrom(location, action)), - ), + PrecheckResult::NotDeterministic(location, action) => { + QueryResult::Consistency(ConsistencyResult::Failure( + ConsistencyFailure::NotDeterministicFrom(location, action), + )) + } PrecheckResult::NotConsistent(failure) => { QueryResult::Consistency(ConsistencyResult::Failure(failure)) } diff --git a/src/System/local_consistency.rs b/src/System/local_consistency.rs index fb425957..e7b08d11 100644 --- a/src/System/local_consistency.rs +++ b/src/System/local_consistency.rs @@ -37,10 +37,18 @@ impl fmt::Display for ConsistencyFailure { ConsistencyFailure::NoInitialLocation => write!(f, "No Initial State"), ConsistencyFailure::EmptyInitialState => write!(f, "Empty Initial State"), ConsistencyFailure::NotConsistentFrom(location, action) => { - write!(f, "Not Consistent From {} Failing action {}", location, action) + write!( + f, + "Not Consistent From {} Failing action {}", + location, action + ) } ConsistencyFailure::NotDeterministicFrom(location, action) => { - write!(f, "Not Deterministic From {} Failing action {}", location, action) + write!( + f, + "Not Deterministic From {} Failing action {}", + location, action + ) } } } @@ -50,15 +58,19 @@ impl fmt::Display for ConsistencyFailure { /// Failure includes the [LocationID]. pub enum DeterminismResult { Success, - Failure(LocationID, String), -} + Failure(LocationID, String), +} impl fmt::Display for DeterminismResult { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { match self { DeterminismResult::Success => write!(f, "Success"), DeterminismResult::Failure(location, action) => { - write!(f, "Not Deterministic From {} failing action {}", location, action) + write!( + f, + "Not Deterministic From {} failing action {}", + location, action + ) } } } @@ -189,7 +201,7 @@ pub fn consistency_least_helper( ); return ConsistencyResult::Failure(failure); } - } else{ + } else { failing_action = input.clone(); } } @@ -214,7 +226,6 @@ pub fn consistency_least_helper( } } } - warn!("failing action {}", failing_action); warn!("No saving outputs from {}", state.get_location().id); ConsistencyResult::Failure(ConsistencyFailure::NotConsistentFrom( state.get_location().id.clone(), @@ -248,7 +259,7 @@ fn consistency_fully_helper( { return ConsistencyResult::Failure(failure); } - } else{ + } else { failing_action = input.clone(); } } @@ -271,12 +282,11 @@ fn consistency_fully_helper( { return ConsistencyResult::Failure(failure); } - } else{ + } else { failing_action = output.clone(); } } } - warn!("failing action {}", failing_action); if output_existed { ConsistencyResult::Success } else { diff --git a/src/System/refine.rs b/src/System/refine.rs index d39d803e..fec98cc4 100644 --- a/src/System/refine.rs +++ b/src/System/refine.rs @@ -55,10 +55,20 @@ impl fmt::Display for RefinementFailure { RefinementFailure::EmptyTransition2s(_) => write!(f, "Empty Transition2s"), RefinementFailure::NotEmptyResult(_) => write!(f, "Not Empty Result on State Pair"), RefinementFailure::ConsistencyFailure(location, action) => { - write!(f, "Not Consistent From {} failing action {}", location.as_ref().unwrap(), action.as_ref().unwrap()) + write!( + f, + "Not Consistent From {} failing action {}", + location.as_ref().unwrap(), + action.as_ref().unwrap() + ) } - RefinementFailure::DeterminismFailure(location, action ) => { - write!(f, "Not Deterministic From {}", location.as_ref().unwrap()) + RefinementFailure::DeterminismFailure(location, action) => { + write!( + f, + "Not Deterministic From {} failing action {}", + location.as_ref().unwrap(), + action.as_ref().unwrap() + ) } } } @@ -554,18 +564,24 @@ fn check_preconditions(sys1: &TransitionSystemPtr, sys2: &TransitionSystemPtr) - PrecheckResult::Success => {} PrecheckResult::NotDeterministic(location, action) => { warn!("Refinement failed - sys1 is not deterministic"); - return RefinementResult::Failure(RefinementFailure::DeterminismFailure(Some(location), Some(action))); + return RefinementResult::Failure(RefinementFailure::DeterminismFailure( + Some(location), + Some(action), + )); } PrecheckResult::NotConsistent(failure) => { warn!("Refinement failed - sys1 is inconsistent"); match failure { ConsistencyFailure::NoInitialLocation | ConsistencyFailure::EmptyInitialState => { - return RefinementResult::Failure(RefinementFailure::ConsistencyFailure(None, None)) + return RefinementResult::Failure(RefinementFailure::ConsistencyFailure( + None, None, + )) } ConsistencyFailure::NotConsistentFrom(location, action) | ConsistencyFailure::NotDeterministicFrom(location, action) => { - return RefinementResult::Failure(RefinementFailure::ConsistencyFailure(Some( - location), Some(action), + return RefinementResult::Failure(RefinementFailure::ConsistencyFailure( + Some(location), + Some(action), )) } } @@ -575,18 +591,24 @@ fn check_preconditions(sys1: &TransitionSystemPtr, sys2: &TransitionSystemPtr) - PrecheckResult::Success => {} PrecheckResult::NotDeterministic(location, action) => { warn!("Refinement failed - sys2 is not deterministic"); - return RefinementResult::Failure(RefinementFailure::DeterminismFailure(Some(location), Some(action))); + return RefinementResult::Failure(RefinementFailure::DeterminismFailure( + Some(location), + Some(action), + )); } PrecheckResult::NotConsistent(failure) => { warn!("Refinement failed - sys2 is inconsistent"); match failure { ConsistencyFailure::NoInitialLocation | ConsistencyFailure::EmptyInitialState => { - return RefinementResult::Failure(RefinementFailure::ConsistencyFailure(None, None)) + return RefinementResult::Failure(RefinementFailure::ConsistencyFailure( + None, None, + )) } ConsistencyFailure::NotConsistentFrom(location, action) | ConsistencyFailure::NotDeterministicFrom(location, action) => { - return RefinementResult::Failure(RefinementFailure::ConsistencyFailure(Some( - location), Some(action), + return RefinementResult::Failure(RefinementFailure::ConsistencyFailure( + Some(location), + Some(action), )) } } From 8fbef488c4985ff568dcd8762b09ec470ca3c0f0 Mon Sep 17 00:00:00 2001 From: Lasse Date: Tue, 8 Nov 2022 10:46:32 +0100 Subject: [PATCH 3/7] Removed TODOs. --- src/System/local_consistency.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/System/local_consistency.rs b/src/System/local_consistency.rs index e7b08d11..af2e5a65 100644 --- a/src/System/local_consistency.rs +++ b/src/System/local_consistency.rs @@ -27,7 +27,7 @@ impl fmt::Display for ConsistencyResult { pub enum ConsistencyFailure { NoInitialLocation, EmptyInitialState, - NotConsistentFrom(LocationID, String), // TODO maybe Option is wrong. + NotConsistentFrom(LocationID, String), NotDeterministicFrom(LocationID, String), } @@ -181,7 +181,7 @@ pub fn consistency_least_helper( if state.decorated_locations.is_inconsistent() { return ConsistencyResult::Failure(ConsistencyFailure::NotConsistentFrom( state.get_location().id.clone(), - failing_action, // TODO FIX. + failing_action, )); } From 0fc9326f0101ddc7b10d59db5e9b5760f3c77991 Mon Sep 17 00:00:00 2001 From: Lasse Date: Wed, 9 Nov 2022 09:53:14 +0100 Subject: [PATCH 4/7] proto --- Ecdar-ProtoBuf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Ecdar-ProtoBuf b/Ecdar-ProtoBuf index c181269f..21c0d2da 160000 --- a/Ecdar-ProtoBuf +++ b/Ecdar-ProtoBuf @@ -1 +1 @@ -Subproject commit c181269f734c85ec51ae7e09de10cb685e54c595 +Subproject commit 21c0d2daaf36404ac4e9f2ec05a13959c792dcb0 From 7289cb46d06575d51a4b419e2e4eb3fba225b04a Mon Sep 17 00:00:00 2001 From: Lasse Date: Wed, 9 Nov 2022 12:11:52 +0100 Subject: [PATCH 5/7] Fixed determinism and consistency failure message tests. --- src/tests/failure_message/consistency_test.rs | 2 +- src/tests/failure_message/determinism_test.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tests/failure_message/consistency_test.rs b/src/tests/failure_message/consistency_test.rs index a7a389b6..bf9e5ab2 100644 --- a/src/tests/failure_message/consistency_test.rs +++ b/src/tests/failure_message/consistency_test.rs @@ -12,7 +12,7 @@ mod test { assert!(matches!( actual, QueryResult::Consistency(ConsistencyResult::Failure( - ConsistencyFailure::NotConsistentFrom(_) + ConsistencyFailure::NotConsistentFrom(_, _) )) )); } diff --git a/src/tests/failure_message/determinism_test.rs b/src/tests/failure_message/determinism_test.rs index 51d11863..abd78df9 100644 --- a/src/tests/failure_message/determinism_test.rs +++ b/src/tests/failure_message/determinism_test.rs @@ -14,7 +14,7 @@ mod test { let actual = json_run_query(PATH, "determinism: NonDeterminismCom"); assert!(matches!( actual, - QueryResult::Determinism(DeterminismResult::Failure(_)) + QueryResult::Determinism(DeterminismResult::Failure(_, _)) )); } @@ -24,7 +24,7 @@ mod test { assert!(matches!( actual, QueryResult::Refinement(RefinementResult::Failure( - RefinementFailure::DeterminismFailure(_) + RefinementFailure::DeterminismFailure(_, _) )) )); } From d8c6d2c1cc562348f5e4539ac44420cd61485a71 Mon Sep 17 00:00:00 2001 From: Lasse Date: Wed, 9 Nov 2022 13:32:49 +0100 Subject: [PATCH 6/7] changed tests from (_, _) to (..) --- src/tests/failure_message/consistency_test.rs | 2 +- src/tests/failure_message/determinism_test.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tests/failure_message/consistency_test.rs b/src/tests/failure_message/consistency_test.rs index bf9e5ab2..8cdddd74 100644 --- a/src/tests/failure_message/consistency_test.rs +++ b/src/tests/failure_message/consistency_test.rs @@ -12,7 +12,7 @@ mod test { assert!(matches!( actual, QueryResult::Consistency(ConsistencyResult::Failure( - ConsistencyFailure::NotConsistentFrom(_, _) + ConsistencyFailure::NotConsistentFrom(..) )) )); } diff --git a/src/tests/failure_message/determinism_test.rs b/src/tests/failure_message/determinism_test.rs index abd78df9..74326430 100644 --- a/src/tests/failure_message/determinism_test.rs +++ b/src/tests/failure_message/determinism_test.rs @@ -14,7 +14,7 @@ mod test { let actual = json_run_query(PATH, "determinism: NonDeterminismCom"); assert!(matches!( actual, - QueryResult::Determinism(DeterminismResult::Failure(_, _)) + QueryResult::Determinism(DeterminismResult::Failure(..)) )); } @@ -24,7 +24,7 @@ mod test { assert!(matches!( actual, QueryResult::Refinement(RefinementResult::Failure( - RefinementFailure::DeterminismFailure(_, _) + RefinementFailure::DeterminismFailure(..) )) )); } From bf13ebfa7a3acf6d98fb948d14bb34a8a2e01435 Mon Sep 17 00:00:00 2001 From: Lasse Date: Wed, 9 Nov 2022 14:13:09 +0100 Subject: [PATCH 7/7] Added comment for empty action string in failure message. --- src/ProtobufServer/ecdar_requests/send_query.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ProtobufServer/ecdar_requests/send_query.rs b/src/ProtobufServer/ecdar_requests/send_query.rs index 3c5f6c66..a965bf52 100644 --- a/src/ProtobufServer/ecdar_requests/send_query.rs +++ b/src/ProtobufServer/ecdar_requests/send_query.rs @@ -153,7 +153,7 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option { reason: "".to_string(), relation: vec![], state: None, - action: "".to_string(), + action: "".to_string(), // Empty string is used, when no failing action is available. })) } refine::RefinementResult::Failure(failure) => convert_refinement_failure(failure),