Skip to content

Commit

Permalink
Merge pull request #103 from Ecdar-SW5/feature/collect-failing-action
Browse files Browse the repository at this point in the history 
Added collection of action string to Determinism, consistency and ref…
  • Loading branch information
@lass5588
lass5588 authored Nov 10, 2022
2 parents 5d1cb6f + bf13ebf commit 0a35d9a
Show file tree
Hide file tree
Showing 12 changed files with 125 additions and 61 deletions.
2 changes: 1 addition & 1 deletion Ecdar-ProtoBuf
Submodule Ecdar-ProtoBuf updated 1 files
+3 −0 query.proto
26 changes: 21 additions & 5 deletions src/ProtobufServer/ecdar_requests/send_query.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,7 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option<ProtobufResult> {
reason: "".to_string(),
relation: vec![],
state: None,
action: "".to_string(), // Empty string is used, when no failing action is available.
}))
}
refine::RefinementResult::Failure(failure) => convert_refinement_failure(failure),
Expand All @@ -173,6 +174,7 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option<ProtobufResult> {
success: true,
reason: "".to_string(),
state: None,
action: "".to_string(),
}))
}
ConsistencyResult::Failure(failure) => match failure {
Expand All @@ -181,10 +183,11 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option<ProtobufResult> {
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(),
Expand All @@ -197,6 +200,7 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option<ProtobufResult> {
}),
federation: None,
}),
action: action.to_string(),
}))
}
},
Expand All @@ -207,9 +211,10 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option<ProtobufResult> {
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(),
Expand All @@ -222,6 +227,7 @@ fn convert_ecdar_result(query_result: &QueryResult) -> Option<ProtobufResult> {
}),
federation: None,
}),
action: action.to_string(),
}))
}
},
Expand All @@ -241,6 +247,7 @@ fn convert_refinement_failure(failure: &RefinementFailure) -> Option<ProtobufRes
relation: vec![],
state: None,
reason: failure.to_string(),
action: "".to_string(),
}))
}
RefinementFailure::CutsDelaySolutions(state_pair)
Expand All @@ -260,10 +267,11 @@ fn convert_refinement_failure(failure: &RefinementFailure) -> Option<ProtobufRes
}),
}),
reason: failure.to_string(),
action: "".to_string(),
}))
}
RefinementFailure::ConsistencyFailure(location_id)
| RefinementFailure::DeterminismFailure(location_id) => {
RefinementFailure::ConsistencyFailure(location_id, action)
| RefinementFailure::DeterminismFailure(location_id, action) => {
Some(ProtobufResult::Refinement(RefinementResult {
success: false,
reason: failure.to_string(),
Expand All @@ -276,6 +284,7 @@ fn convert_refinement_failure(failure: &RefinementFailure) -> Option<ProtobufRes
}),
federation: None,
}),
action: value_in_action(action),
relation: vec![],
}))
}
Expand Down Expand Up @@ -332,3 +341,10 @@ fn value_in_location(maybe_location: &Option<LocationID>) -> String {
None => "".to_string(),
}
}

fn value_in_action(maybe_action: &Option<String>) -> String {
match maybe_action {
Some(action) => action.to_string(),
None => "".to_string(),
}
}
10 changes: 6 additions & 4 deletions src/System/executable_query.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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) => 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))
}
Expand Down
56 changes: 42 additions & 14 deletions src/System/local_consistency.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,20 +27,28 @@ impl fmt::Display for ConsistencyResult {
pub enum ConsistencyFailure {
NoInitialLocation,
EmptyInitialState,
NotConsistentFrom(LocationID),
NotDeterministicFrom(LocationID),
NotConsistentFrom(LocationID, String),
NotDeterministicFrom(LocationID, String),
}

impl fmt::Display for ConsistencyFailure {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
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
)
}
}
}
Expand All @@ -50,15 +58,19 @@ 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
)
}
}
}
Expand Down Expand Up @@ -117,18 +129,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);
}
}
}
Expand Down Expand Up @@ -157,6 +170,8 @@ pub fn consistency_least_helper(
passed_list: &mut Vec<State>,
system: &dyn TransitionSystem,
) -> ConsistencyResult {
let mut failing_action = String::new();

if state.is_contained_in_list(passed_list) {
return ConsistencyResult::Success;
}
Expand All @@ -166,6 +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,
));
}

Expand All @@ -185,6 +201,8 @@ pub fn consistency_least_helper(
);
return ConsistencyResult::Failure(failure);
}
} else {
failing_action = input.clone();
}
}
}
Expand All @@ -203,12 +221,15 @@ pub fn consistency_least_helper(
{
return ConsistencyResult::Success;
}
} else {
failing_action = output.clone();
}
}
}
warn!("No saving outputs from {}", state.get_location().id);
ConsistencyResult::Failure(ConsistencyFailure::NotConsistentFrom(
state.get_location().id.clone(),
failing_action,
))
}

Expand All @@ -218,6 +239,8 @@ fn consistency_fully_helper(
passed_list: &mut Vec<State>,
system: &dyn TransitionSystem,
) -> ConsistencyResult {
let mut failing_action = String::new();

if state.is_contained_in_list(passed_list) {
return ConsistencyResult::Success;
}
Expand All @@ -236,6 +259,8 @@ fn consistency_fully_helper(
{
return ConsistencyResult::Failure(failure);
}
} else {
failing_action = input.clone();
}
}
}
Expand All @@ -257,6 +282,8 @@ fn consistency_fully_helper(
{
return ConsistencyResult::Failure(failure);
}
} else {
failing_action = output.clone();
}
}
}
Expand All @@ -267,6 +294,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,
}
Expand Down
2 changes: 1 addition & 1 deletion src/System/pruning.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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")
Expand Down
Loading

0 comments on commit 0a35d9a

Please sign in to comment.