Skip to content

Commit

Permalink
Merge pull request #134 from Ecdar-SW5/ccof_actions_test
Browse files Browse the repository at this point in the history 
Ccof actions test
  • Loading branch information
@VictorDore
VictorDore authored Nov 21, 2022
2 parents 93be4c7 + 69d248b commit e7d4351
Show file tree
Hide file tree
Showing 9 changed files with 787 additions and 0 deletions.
414 changes: 414 additions & 0 deletions samples/json/Actions/Components/CorrectComponent.json
View file

Large diffs are not rendered by default.

71 changes: 71 additions & 0 deletions samples/json/Actions/Components/NonConsistent.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
{
"name": "notConsistent",
"declarations": "clock u;",
"locations": [
{
"id": "L16",
"nickname": "",
"invariant": "",
"type": "INITIAL",
"urgency": "NORMAL",
"x": 120.0,
"y": 120.0,
"color": "6",
"nicknameX": 30.0,
"nicknameY": -10.0,
"invariantX": 30.0,
"invariantY": 10.0
},
{
"id": "L17",
"nickname": "",
"invariant": "u\u003c1",
"type": "NORMAL",
"urgency": "NORMAL",
"x": 320.00001,
"y": 120.0,
"color": "6",
"nicknameX": 30.0,
"nicknameY": -10.0,
"invariantX": 30.0,
"invariantY": 10.0
}
],
"edges": [
{
"id": "E0",
"group": "",
"sourceLocation": "L16",
"targetLocation": "L17",
"status": "INPUT",
"select": "",
"guard": "u \u003c1",
"update": "",
"sync": "coffee",
"isLocked": false,
"nails": [
{
"x": 180.0,
"y": 120.0,
"propertyType": "GUARD",
"propertyX": 10.0,
"propertyY": 0.0
},
{
"x": 240.46740467404675,
"y": 118.65928659286593,
"propertyType": "SYNCHRONIZATION",
"propertyX": 10.0,
"propertyY": 0.0
}
]
}
],
"description": "",
"x": 88.8,
"y": 152.0,
"width": 450.0,
"height": 240.0,
"color": "6",
"includeInPeriodicCheck": false
}
99 changes: 99 additions & 0 deletions samples/json/Actions/Components/NonDeterministic1.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
{
"name": "NonDeterminismCom",
"declarations": "",
"locations": [
{
"id": "L1",
"nickname": "",
"invariant": "",
"type": "INITIAL",
"urgency": "NORMAL",
"x": 205.0,
"y": 300.0,
"color": "2",
"nicknameX": 30.0,
"nicknameY": -10.0,
"invariantX": 30.0,
"invariantY": 10.0
},
{
"id": "L2",
"nickname": "",
"invariant": "",
"type": "NORMAL",
"urgency": "NORMAL",
"x": 330.00001,
"y": 326.0,
"color": "2",
"nicknameX": 30.0,
"nicknameY": -10.0,
"invariantX": 30.0,
"invariantY": 10.0
},
{
"id": "L3",
"nickname": "",
"invariant": "",
"type": "NORMAL",
"urgency": "NORMAL",
"x": 320.00001,
"y": 244.24999999999997,
"color": "2",
"nicknameX": 30.0,
"nicknameY": -10.0,
"invariantX": 30.0,
"invariantY": 10.0
}
],
"edges": [
{
"id": "E0",
"group": "",
"sourceLocation": "L1",
"targetLocation": "L2",
"status": "INPUT",
"select": "",
"guard": "",
"update": "",
"sync": "1",
"isLocked": false,
"nails": [
{
"x": 263.66666666666663,
"y": 330.75,
"propertyType": "SYNCHRONIZATION",
"propertyX": 10.0,
"propertyY": 0.0
}
]
},
{
"id": "E1",
"group": "",
"sourceLocation": "L1",
"targetLocation": "L3",
"status": "INPUT",
"select": "",
"guard": "",
"update": "",
"sync": "1",
"isLocked": false,
"nails": [
{
"x": 244.83333333333331,
"y": 253.08333333333331,
"propertyType": "SYNCHRONIZATION",
"propertyX": 10.0,
"propertyY": 0.0
}
]
}
],
"description": "",
"x": 257.0,
"y": 43.0,
"width": 450.0,
"height": 600.0,
"color": "2",
"includeInPeriodicCheck": true
}
99 changes: 99 additions & 0 deletions samples/json/Actions/Components/NonDeterministic2.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,99 @@
{
"name": "Component2",
"declarations": "",
"locations": [
{
"id": "L0",
"nickname": "",
"invariant": "",
"type": "INITIAL",
"urgency": "NORMAL",
"x": 165.0,
"y": 290.0,
"color": "4",
"nicknameX": 30.0,
"nicknameY": -10.0,
"invariantX": 30.0,
"invariantY": 10.0
},
{
"id": "L1",
"nickname": "",
"invariant": "",
"type": "NORMAL",
"urgency": "NORMAL",
"x": 270.00001,
"y": 231.33333333333331,
"color": "4",
"nicknameX": 30.0,
"nicknameY": -10.0,
"invariantX": 30.0,
"invariantY": 10.0
},
{
"id": "L2",
"nickname": "",
"invariant": "",
"type": "NORMAL",
"urgency": "NORMAL",
"x": 270.00001,
"y": 309.5833333333333,
"color": "4",
"nicknameX": 30.0,
"nicknameY": -10.0,
"invariantX": 30.0,
"invariantY": 10.0
}
],
"edges": [
{
"id": "E0",
"group": "",
"sourceLocation": "L0",
"targetLocation": "L2",
"status": "INPUT",
"select": "",
"guard": "",
"update": "",
"sync": "1",
"isLocked": false,
"nails": [
{
"x": 186.0,
"y": 311.91666666666663,
"propertyType": "SYNCHRONIZATION",
"propertyX": 10.0,
"propertyY": 0.0
}
]
},
{
"id": "E1",
"group": "",
"sourceLocation": "L0",
"targetLocation": "L1",
"status": "INPUT",
"select": "",
"guard": "",
"update": "",
"sync": "2",
"isLocked": false,
"nails": [
{
"x": 188.33333333333331,
"y": 254.24999999999997,
"propertyType": "SYNCHRONIZATION",
"propertyX": 10.0,
"propertyY": 0.0
}
]
}
],
"description": "",
"x": 257.0,
"y": 43.0,
"width": 450.0,
"height": 600.0,
"color": "4",
"includeInPeriodicCheck": true
}
2 changes: 2 additions & 0 deletions samples/json/Actions/Queries.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
[
]
4 changes: 4 additions & 0 deletions samples/json/Actions/SystemDeclarations.json
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
{
"name": "System Declarations",
"declarations": "system NonDeterministic1, NonDeterministic2, NonConsistent, CorrectComponent;\n"
}
96 changes: 96 additions & 0 deletions src/tests/failure_message/actions_test.rs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
#[cfg(test)]

mod test {

use crate::tests::refinement::Helper::json_run_query;
use crate::System::{
executable_query::QueryResult,
local_consistency::{ConsistencyFailure, ConsistencyResult, DeterminismResult},
refine::{RefinementFailure, RefinementResult},
};
use crate::TransitionSystems::LocationID;

const PATH: &str = "samples/json/Actions";

#[test]
fn determinism_test() {
let expected_action = String::from("1");
let expected_location = LocationID::Simple {
location_id: (String::from("L1")),
component_id: Some(String::from("NonDeterminismCom")),
};
if let QueryResult::Determinism(DeterminismResult::Failure(
actual_location,
actual_action,
)) = json_run_query(PATH, "determinism: NonDeterministic1")
{
assert_eq!(
(expected_location, expected_action),
(actual_location, actual_action)
);
} else {
panic!("Models in saples/action have been changed, REVERT!");
}
}

#[test]
fn not_consistent_from_test() {
let expected_action = String::from("");
let expected_location = LocationID::Simple {
location_id: (String::from("L17")),
component_id: Some(String::from("notConsistent")),
};
if let QueryResult::Consistency(ConsistencyResult::Failure(
ConsistencyFailure::NotConsistentFrom(actual_location, actual_action),
)) = json_run_query(PATH, "consistency: NonConsistent")
{
assert_eq!(
(expected_location, expected_action),
(actual_location, actual_action)
);
} else {
panic!("Models in saples/action have been changed, REVERT!");
}
}

#[test]
fn refinement_determinism_test() {
let expected_action = String::from("1");
let expected_location = LocationID::Simple {
location_id: (String::from("L1")),
component_id: Some(String::from("NonDeterminismCom")),
};
if let QueryResult::Refinement(RefinementResult::Failure(
RefinementFailure::DeterminismFailure(actual_location, actual_action),
)) = json_run_query(PATH, "refinement: NonDeterministic1 <= NonDeterministic2")
{
assert_eq!(
(expected_location, expected_action),
(actual_location.unwrap(), actual_action.unwrap())
);
} else {
panic!("Models in saples/action have been changed, REVERT!");
}
}

#[test]
fn refinement_consistency_test() {
let expected_action = String::from("");
let expected_location = LocationID::Simple {
location_id: (String::from("L17")),
component_id: Some(String::from("notConsistent")),
};

if let QueryResult::Refinement(RefinementResult::Failure(
RefinementFailure::ConsistencyFailure(actual_location, actual_action),
)) = json_run_query(PATH, "refinement: NonConsistent <= CorrectComponent")
{
assert_eq!(
(expected_location, expected_action),
(actual_location.unwrap(), actual_action.unwrap())
);
} else {
panic!("Models in saples/action have been changed, REVERT!");
}
}
}
1 change: 1 addition & 0 deletions src/tests/failure_message/determinism_test.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ mod test {
#[test]
fn determinism_failure_test() {
let actual = json_run_query(PATH, "determinism: NonDeterminismCom");

assert!(matches!(
actual,
QueryResult::Determinism(DeterminismResult::Failure(..))
Expand Down
1 change: 1 addition & 0 deletions src/tests/failure_message/mod.rs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
pub mod actions_test;
pub mod consistency_test;
pub mod determinism_test;
pub mod refinement_test;

0 comments on commit e7d4351

Please sign in to comment.