Simulation (#55)

* Update test comment * Format * Revert "xd" This reverts commit 556b8a8. * Manually fix residue conflicts… thanks Nicolai * Manually fix residue conflicts… thanks Nicolai * Still fixing * Still fixing * Fix compiler errors * Fix compiler warnings, and format * Fix compiler error * Update some tests, now passig :) * fmt * Refactor * Refactor * Preperation for next sprint * Multiple: - Add id to Edge - Test and implement \`from :: TransitionDecisionPoint -> DecisionPoint\` - Remove common helper function for Simulation testing to file in test dir * started testing * Works now * Implemented take_simulation_steps and refactored some code into simulation_info_to_transition_system helper function * Working on tests for DecisionPoint -> ProtoDecisionPoint * Remove unused code * Fix tests that failed because id was added to edge * Add test from__good_DecisionPoint__returns_good_ProtoDecisionPoint * TransitionDecision_from__Decision__returns_correct_TransitionDecision() 🧪 * No idea why I had to track these files again. * Added another failingfailing test Decision_from__ProtoDecision__returns_correct_Decision() 🧪 * Getting ready to implement * formatted * Start implement from :: (&DecisionPoint, &TransitionSystemPtr) -> ProtoDecisionPoint * Delete decisionpoint_serializer.rs * Working on test for ProtoDecisionPoint * Implementing from ProtoDecision to Decision * Test for ProtoDecisionPoint fixed * Implementation begun on transition_decision_point.rs * Cleanup * Move TransitionDecision to own file * Move Decision to own file * fmt * Update test names * Test pass and working implementation (needs reviewing) * Fix requested changes * Added slight documentation * Fix compile error * Merged main * . * Create federation from proto_decision * . * Fix from :: &Decision, &TransitionSystemPtr -> TransitionDecision * Refactor * Update documentation * Update documentation * ProtoEdge can find specific component * Update proto * Update proto * Fix compiler warning and errors * added component_name field to edge * Refactor from :: (&Decision, &TransitionSystemPrt) -> TransitionDecision * Multithread start_simulation api * Revert "Merge branch 'main' into Simulation" This reverts commit bc9ed6e, reversing changes made to bedb80d. * Change branch * Not building XD * implement find state (maybe?) * Added some implementation to Protoconstraint::from(constraint) * Revert "Revert "Merge branch 'main' into Simulation"" This reverts commit 62552d1. * Fix compiler error * Change from :: &Transition -> [Edge] to return empty [] * Unignore test start_simulation__responds_as_expected * Refactor * Work on from :: (&Constraint, &TransitionSystemPtr) -> ProtoConstraint * Correct Some tests * Fix compiler error * Fix bug in from :: Decision -> TransitionDecision * Encapsulate all Simulation structs * Refactor confusing function * Remove allow dead code * Fix compiler errors * Remove incorrect comment * Update error message * Replace unwrap() with match * Finish from :: &TransitionDecisionPoin -> DecisionPoint * Fix clippy * Do something i dont remeber * Working on ProtoDecision -> Decision, Clocks not working * Implement component_names for trait TransitionSystem * Ignore failing tests * Remove unused test module * I don't even know * Write test for composition * Fix warnings * EOD, test fixed and working on logic * Write tests for composition components * Write tests for composition components * Fix bug, tests still failing it works tho * Move test `start_simulation_step__get_composit_component__should_return_component` - Also fix decision point to order, so same result every time * Write passing tests for conjunction components * Test/Logic working on Decision::from(ProtoDecision) * Working on more tests. my friends! * Refactor and maybe fix bug * Working on tests once again! * Format * Write failing tests for take_simulation_step * Fix warnings and format * Fix warnings and format * Fix compiler warnings * This does not build! Logic * . * Fix bug and ignore tests that hang * Fix test * Fix clippy * Implement non-deterministic choises internally * Update proto * Format * Move stuff that create proto structs to proto_writer * Move stuff that creates stuff from proto objects * Remove unused test mod * Refactor * Fixed take_simulation_step__get_composit_component__should_return_component test Conjunction test is still ignored for now * filter hidden edges * take_simulation_step__get_composit_component__should_return_component for conjunction Also fixed error in previous commit that made some tests fail * Refactor * Create propterbased test B) * Add test * Create test and found bug :( * Refactor * Refactor * Refactor * Fix clippy: * Fix bug where hidden edges would not be filtered * Remove .clone() * Rename variable * Create baller integration test * format * Remove print line from test * Moved Proto_location_tuple_to_location_tuple to ProtoReader * Combine tests under same case * Combine test cases * Move test data to test_data.rs * Move test data from take_simultion_step.rs to test_data.rs * Move test data from start_simulation.rs to test_data.rs * split grpc_helper.rs into test_data.rs and helper.rs * Fix compiler warnings * Format * Move helpers functions from simulation.rs to helper.rs * Refactor and update documentation * Add documentation * Add documentation to handle_take_simulation_step * Update documentation : * Replace match with unwrap * Revert "Replace match with unwrap" This reverts commit 61c4fb8. * Add documentation * Document decision.rs * Document decision_point.rs * Update documentation * Update documentation * Change resolve to return None when use_transition is false * Unignore from_Determinism_NonDeterminismCom__returns_ok * ^ * Unignore and update test and make test module private * Refactor component.rs * Fix clippy * Fix clippy * Update documentation * Update documentation and naming * Update documentation * Refactor and update documentation * Remove unused use * Refactor proto_writer.rs * Document proto_writer.rs * Update uncomment test * Document and refactor proto_reader.rs * more documentation and refactoring * Fix clippy * Refactor * Fix clippy * Refactor and document Decision::resolve * Refactor and document DecisionPoint::initial * Add test for non-convex federation for state_to_proto_state_to_state_is_same_state * Remove commented code * ^ * Refactor proto_decision_to_decision__ProtoDecision_with_universal_ProtoFederation__returns_correct_Decision * proto_decision_to_decision__ProtoDecision_with_nonuniversal_ProtoFederation__returns_correct_Decision * Refactor proto_decision_to_decision__ProtoDecision_with_conjunction_of_components__returns_correct_Decision * Refactor decision_point_to_proto_decision_point__initial_DecisionPoint_EcdarUniversity_Administration_par_Machine_par_Researcher__returns_correct_ProtoDecisionPoint * Refactor decision_point_to_proto_decision_point__initial_DecisionPoint_EcdarUniversity_Machine__returns_correct_ProtoDecisionPoint * Refactor decision_point_to_proto_decision_point__initial_DecisionPoint_EcdarUniversity_Machine_after_tea__returns_correct_ProtoDecisionPoint * Move test * Refactor from__initial_EcdarUniversity_Machine__returns_correct_DecisionPoint * Refactor testing * Refactor test * Add TODO * Make test module private * Refactor * Document decision_point_to_proto_decision_point() * Remove unused dependencie * Add bench for Simulation * Fix clippy * Refactor * Fixed test name to be accurate * Move .sorted() to sort less elements * Refactor proto_location_tuple_to_location_tuple as mentioned in review * Declare constant as const * Create alternative use_transition Co-authored-by: Mightyhaha <74659365+Mightyhaha@users.noreply.github.com> Co-authored-by: Patrick Bertelsen <pberte20@users.noreply.github.com> Co-authored-by: Simon Andersen <smpandersen@gmail.com> Co-authored-by: Mads Balslev <madspbalslev@gmail.com> Co-authored-by: pberte20 <71381584+pberte20@users.noreply.github.com>
Ecdar-SW5 · Dec 7, 2022 · a3618c8 · a3618c8
1 parent c4304c4
commit a3618c8
Show file tree

Hide file tree

Showing 35 changed files with 3,570 additions and 14 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -39,9 +39,12 @@ edbm = { git = "https://github.com/Ecdar/EDBM" }
 log = "0.4.17"
 env_logger = { version = "0.9.0", optional = true }
 chrono = { version = "0.4.22", optional = true }
+test-case = "2.2.2"
 crossbeam-channel = "0.5.6"
 num_cpus = "1.13.1"
 lru = "0.8.1"
+itertools = "0.10.5"
+regex = "1"
 
 # Enable optimizations for EDBM in debug mode, but not for our code:
 [profile.dev.package.edbm]
@@ -71,4 +74,8 @@ harness = false
 
 [[bench]]
 name = "clock_reduction_bench"
+harness = false
+
+[[bench]]
+name = "simulation_bench"
 harness = false
diff --git a/benches/simulation_bench.rs b/benches/simulation_bench.rs
@@ -0,0 +1,122 @@
+use criterion::{criterion_group, criterion_main, Criterion};
+pub mod flamegraph;
+use flamegraph::flamegraph_profiler::FlamegraphProfiler;
+use reveaal::{
+    tests::Simulation::helper,
+    DataReader::component_loader::ModelCache,
+    ProtobufServer::{
+        services::{SimulationStartRequest, SimulationStepRequest},
+        ConcreteEcdarBackend,
+    },
+};
+use tonic::Response;
+
+static PATH: &str = "samples/json/EcdarUniversity";
+
+fn create_step_request(
+    component_names: &[&str],
+    components_path: &str,
+    composition: &str,
+    last_response: &SimulationStartRequest,
+) -> SimulationStepRequest {
+    let cache = ModelCache::default();
+    helper::create_step_request(
+        component_names,
+        components_path,
+        composition,
+        ConcreteEcdarBackend::handle_start_simulation(last_response.clone(), cache)
+            .map(Response::new),
+    )
+}
+
+fn start_simulation(c: &mut Criterion, id: &str, request: SimulationStartRequest) {
+    let cache = ModelCache::default();
+    c.bench_function(id, |b| {
+        b.iter(|| ConcreteEcdarBackend::handle_start_simulation(request.to_owned(), cache.clone()))
+    });
+}
+
+fn take_simulation_step(c: &mut Criterion, id: &str, request: SimulationStepRequest) {
+    let cache = ModelCache::default();
+    c.bench_function(id, |b| {
+        b.iter(|| ConcreteEcdarBackend::handle_take_simulation_step(request.clone(), cache.clone()))
+    });
+}
+
+fn simulation(c: &mut Criterion) {
+    let start_request_1 = helper::create_start_request(&["Machine"], PATH, "(Machine)");
+    let start_request_2 =
+        helper::create_start_request(&["HalfAdm1", "HalfAdm2"], PATH, "(HalfAdm1 && HalfAdm2)");
+    let start_request_3 = helper::create_start_request(
+        &["Administration", "Machine", "Researcher"],
+        PATH,
+        "(Administration || Machine || Researcher)",
+    );
+    let start_request_4 = helper::create_start_request(
+        &["HalfAdm1", "HalfAdm2", "Machine", "Researcher"],
+        "samples/json/EcdarUniversity",
+        "((HalfAdm1 && HalfAdm2) || Machine || Researcher)",
+    );
+
+    let step_request_1 = create_step_request(&["Machine"], PATH, "(Machine)", &start_request_1);
+    let step_request_2 = create_step_request(
+        &["HalfAdm1", "HalfAdm2"],
+        PATH,
+        "(HalfAdm1 && HalfAdm2)",
+        &start_request_2,
+    );
+    let step_request_3 = create_step_request(
+        &["Administration", "Machine", "Researcher"],
+        PATH,
+        "(Administration || Machine || Researcher)",
+        &start_request_3,
+    );
+    let step_request_4 = create_step_request(
+        &["HalfAdm1", "HalfAdm2", "Machine", "Researcher"],
+        "samples/json/EcdarUniversity",
+        "((HalfAdm1 && HalfAdm2) || Machine || Researcher)",
+        &start_request_4,
+    );
+
+    start_simulation(c, "start simulation for (Machine)", start_request_1);
+    start_simulation(
+        c,
+        "start simulation for (HalfAdm1 && HalfAdm2)",
+        start_request_2,
+    );
+    start_simulation(
+        c,
+        "start simulation for (Administration || Machine || Researcher)",
+        start_request_3,
+    );
+    start_simulation(
+        c,
+        "start simulation for ((HalfAdm1 && HalfAdm2) || Machine || Researcher)",
+        start_request_4,
+    );
+
+    take_simulation_step(c, "take simulation step for (Machine)", step_request_1);
+    take_simulation_step(
+        c,
+        "take simulation step for (HalfAdm1 && HalfAdm2)",
+        step_request_2,
+    );
+    take_simulation_step(
+        c,
+        "take simulation step for (Administration || Machine || Researcher)",
+        step_request_3,
+    );
+    take_simulation_step(
+        c,
+        "take simulation step for ((HalfAdm1 && HalfAdm2) || Machine || Researcher)",
+        step_request_4,
+    );
+}
+
+criterion_group! {
+  name = simulation_benches;
+  config = Criterion::default().with_profiler(FlamegraphProfiler::new(100));
+  targets = simulation
+}
+
+criterion_main!(simulation_benches);
diff --git a/samples/json/EcdarUniversity/Components/Machine4.json b/samples/json/EcdarUniversity/Components/Machine4.json
@@ -0,0 +1,176 @@
+{
+  "name": "Machine4",
+  "declarations": "clock y;",
+  "locations": [
+    {
+      "id": "L4",
+      "nickname": "",
+      "invariant": "y\u003c\u003d6",
+      "type": "NORMAL",
+      "urgency": "NORMAL",
+      "x": 140.0,
+      "y": 300.0,
+      "color": "7",
+      "nicknameX": 30.0,
+      "nicknameY": -10.0,
+      "invariantX": 30.0,
+      "invariantY": -10.0
+    },
+    {
+      "id": "L5",
+      "nickname": "",
+      "invariant": "",
+      "type": "INITIAL",
+      "urgency": "NORMAL",
+      "x": 140.0,
+      "y": 100.0,
+      "color": "7",
+      "nicknameX": 30.0,
+      "nicknameY": -10.0,
+      "invariantX": 30.0,
+      "invariantY": 10.0
+    }
+  ],
+  "edges": [
+    {
+      "id": "E1",
+      "group": "",
+      "sourceLocation": "L4",
+      "targetLocation": "L5",
+      "status": "OUTPUT",
+      "select": "",
+      "guard": "y\u003e\u003d4",
+      "update": "",
+      "sync": "cof",
+      "isLocked": false,
+      "nails": [
+        {
+          "x": 100.0,
+          "y": 230.0,
+          "propertyType": "GUARD",
+          "propertyX": -70.0,
+          "propertyY": -10.0
+        },
+        {
+          "x": 100.0,
+          "y": 180.0,
+          "propertyType": "SYNCHRONIZATION",
+          "propertyX": -70.0,
+          "propertyY": -10.0
+        }
+      ]
+    },
+    {
+      "id": "E2",
+      "group": "",
+      "sourceLocation": "L4",
+      "targetLocation": "L5",
+      "status": "OUTPUT",
+      "select": "",
+      "guard": "",
+      "update": "",
+      "sync": "tea",
+      "isLocked": false,
+      "nails": [
+        {
+          "x": 210.0,
+          "y": 200.0,
+          "propertyType": "SYNCHRONIZATION",
+          "propertyX": 20.0,
+          "propertyY": -10.0
+        }
+      ]
+    },
+    {
+      "id": "E3",
+      "group": "",
+      "sourceLocation": "L5",
+      "targetLocation": "L4",
+      "status": "INPUT",
+      "select": "",
+      "guard": "",
+      "update": "y\u003d0",
+      "sync": "coin",
+      "isLocked": false,
+      "nails": [
+        {
+          "x": 140.0,
+          "y": 220.0,
+          "propertyType": "SYNCHRONIZATION",
+          "propertyX": 20.0,
+          "propertyY": -10.0
+        },
+        {
+          "x": 140.0,
+          "y": 190.0,
+          "propertyType": "UPDATE",
+          "propertyX": 10.0,
+          "propertyY": -10.0
+        }
+      ]
+    },
+    {
+      "id": "E4",
+      "group": "",
+      "sourceLocation": "L4",
+      "targetLocation": "L4",
+      "status": "INPUT",
+      "select": "",
+      "guard": "",
+      "update": "",
+      "sync": "coin",
+      "isLocked": false,
+      "nails": [
+        {
+          "x": 130.0,
+          "y": 350.0,
+          "propertyType": "SYNCHRONIZATION",
+          "propertyX": -60.0,
+          "propertyY": -10.0
+        },
+        {
+          "x": 160.0,
+          "y": 350.0,
+          "propertyType": "NONE",
+          "propertyX": 0.0,
+          "propertyY": 0.0
+        }
+      ]
+    },
+    {
+      "id": "E5",
+      "group": "",
+      "sourceLocation": "L5",
+      "targetLocation": "L5",
+      "status": "OUTPUT",
+      "select": "",
+      "guard": "y\u003c0",
+      "update": "",
+      "sync": "tea",
+      "isLocked": false,
+      "nails": [
+        {
+          "x": 170.0,
+          "y": 60.0,
+          "propertyType": "GUARD",
+          "propertyX": 10.0,
+          "propertyY": -20.0
+        },
+        {
+          "x": 140.0,
+          "y": 60.0,
+          "propertyType": "SYNCHRONIZATION",
+          "propertyX": -20.0,
+          "propertyY": -30.0
+        }
+      ]
+    }
+  ],
+  "description": "",
+  "x": 5.0,
+  "y": 5.0,
+  "width": 300.0,
+  "height": 390.0,
+  "color": "7",
+  "includeInPeriodicCheck": false
+}
diff --git a/samples/json/EcdarUniversity/SystemDeclarations.json b/samples/json/EcdarUniversity/SystemDeclarations.json
@@ -1,4 +1,4 @@
 {
   "name": "System Declarations",
-  "declarations": "system Spec, Machine, Machine2, Machine3, Administration, HalfAdm1, HalfAdm2, Researcher, Adm2;\nIO Spec { grant?, patent! }\nIO Machine { coin?, tea!, cof! }\nIO Machine2 { coin?, tea!, cof! }\nIO Machine3 { coin?, tea!, cof! }\nIO Administration { grant?, pub?, coin!, patent! }\nIO HalfAdm1 { grant?, pub?, coin!, patent! }\nIO HalfAdm2 { grant?, pub?, coin!, patent! }\nIO Researcher { cof?, tea?, pub! }\nIO Adm2 {grant?, pub?, coin!, patent!}"
+  "declarations": "system Spec, Machine, Machine2, Machine3, Machine4, Administration, HalfAdm1, HalfAdm2, Researcher, Adm2;\nIO Spec { grant?, patent! }\nIO Machine { coin?, tea!, cof! }\nIO Machine2 { coin?, tea!, cof! }\nIO Machine3 { coin?, tea!, cof! }\nIO Administration { grant?, pub?, coin!, patent! }\nIO HalfAdm1 { grant?, pub?, coin!, patent! }\nIO HalfAdm2 { grant?, pub?, coin!, patent! }\nIO Researcher { cof?, tea?, pub! }\nIO Adm2 {grant?, pub?, coin!, patent!}"
 }
diff --git a/samples/json/Simulation/Components/NonConvexFederation.json b/samples/json/Simulation/Components/NonConvexFederation.json
@@ -0,0 +1,28 @@
+{
+    "name": "NonConvexFederation",
+    "declarations": "clock x;",
+    "locations": [
+        {
+            "id": "L4",
+            "nickname": "",
+            "invariant": "x < 2 || x > 4",
+            "type": "INITIAL",
+            "urgency": "NORMAL",
+            "x": 0,
+            "y": 0,
+            "color": "0",
+            "nicknameX": 0,
+            "nicknameY": 0,
+            "invariantX": 0,
+            "invariantY": 0
+        }
+    ],
+    "edges": [],
+    "description": "",
+    "x": 0,
+    "y": 0,
+    "width": 0,
+    "height": 0,
+    "color": "0",
+    "includeInPeriodicCheck": false
+}