Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor for query results and failures, new protobuf protocol, fixing simulation/reachability #147

Merged
merged 56 commits into from
Apr 6, 2023
Merged
Show file tree
Hide file tree
Changes from 42 commits
Commits
Show all changes
56 commits
Select commit Hold shift + click to select a range
e5d0777
Ensure that components have the same file name as name field in json
seblund Feb 1, 2023
bb5399e
Add intermediate 'specific' structs between protobuf objects and Mode…
seblund Feb 1, 2023
d27db39
Introduce QueryResult enum with nicely structured query failures and …
seblund Feb 1, 2023
eae937b
Add method to convert a transition system to a string
seblund Mar 1, 2023
8203940
Add method to get a tree structure of the ComponentInfos in a Transit…
seblund Mar 1, 2023
50b0969
Change proto branch to use the new definitions
seblund Mar 1, 2023
81fc378
Change Decision to be a state and action. Removing the need for Decis…
seblund Mar 1, 2023
edb15a2
Use new Decision struct in reachability paths
seblund Mar 1, 2023
5e71ba1
Update 'specifics' to match new Proto definitions
seblund Mar 1, 2023
85c236d
Update query failures to use new specifics
seblund Mar 1, 2023
112182f
Use new specifics and failures in ExecutableQueries
seblund Mar 1, 2023
8b0f5f0
Implement necessary protobuf conversions
seblund Mar 1, 2023
7f1eb03
Use new result types in all TransitionSystem definitions
seblund Mar 1, 2023
c8cb39b
Use new result types in refinement, simplifying the code
seblund Mar 1, 2023
2744fd6
Fix lib.rs and main.rs with new error types
seblund Mar 1, 2023
3244f84
Add trivial check to fail reachability if states are empty
seblund Mar 1, 2023
9701b6b
Update to use new error and result types
seblund Mar 1, 2023
5d56958
Box parsing errors to avoid clippy warnings
seblund Mar 1, 2023
dae4e77
Add utility method to State struct
seblund Mar 1, 2023
9e4d75d
Simplify code
seblund Mar 1, 2023
7b94453
Use proto conversions from proto_conversions.rs to convert query results
seblund Mar 1, 2023
ae8b4a7
Use new conversion methods in simulation backend implementation
seblund Mar 1, 2023
d16476f
Fix benches after code changes
seblund Mar 1, 2023
30628ed
Update GRPC tests, removing confusing simulation tests (we'll replace…
seblund Mar 1, 2023
affceb4
Change code to match edge formatting
seblund Mar 1, 2023
dd7fb2e
Use new CompiledComponent::compile in tests, setting the component id…
seblund Mar 1, 2023
4f298ca
Update simulation tests and remove confusing simulation test data (mo…
seblund Mar 1, 2023
b0fc5d0
Update refinement tests after result code changes
seblund Mar 1, 2023
c1e6375
Update reachability tests after refactor
seblund Mar 1, 2023
d08966a
Update failure message tests after refactor
seblund Mar 1, 2023
8c8b1a6
Update system recipe tests after refactor
seblund Mar 1, 2023
a9e4e7d
Update save comp tests after refactor
seblund Mar 1, 2023
6e5c0b2
Update protobuf submodule
seblund Mar 2, 2023
8399dbe
Fix weird rustfmt error
seblund Mar 2, 2023
85d26d2
Make LocationType derive Copy
seblund Mar 2, 2023
cacc822
Remove special handling for Universal and Inconsistent as it was wron…
seblund Mar 2, 2023
d6ff918
Remove unnecessary trivial LocationType check from reachability (it d…
seblund Mar 2, 2023
999d5e8
Remove unused method
seblund Mar 2, 2023
597f8e3
Add method to update a State's zone with a closure
seblund Mar 3, 2023
448b9d4
Add destination state to all Decision structs
seblund Mar 3, 2023
0a2a81e
Make take/set zone private methods and use update_zone instead
seblund Mar 3, 2023
23e8bde
Clarify and fix todos
seblund Mar 3, 2023
44db95e
Remove unused id field from SpecificClock
seblund Mar 8, 2023
5345c63
Add documentation to intermediate representations
seblund Mar 8, 2023
7ac9577
Rename LocationTuple to LocationTree
seblund Mar 9, 2023
394bb54
Rename occurences of 'location_tuple' to 'location_tree'
seblund Mar 9, 2023
b88f4e4
Chain ifs in refinement precond to avoid multiple returns
seblund Mar 9, 2023
188fd0c
Rename specific_clock_comp_map2
seblund Mar 9, 2023
ef85999
Rename Composition to SystemType
seblund Mar 9, 2023
192d4fa
Simplify is_least_consistent
seblund Mar 9, 2023
c250819
Avoid using return in handle_send_query
seblund Mar 9, 2023
08e447d
Add documentation to all structs and methods in query_failures.rs
seblund Mar 9, 2023
a1fd8f4
Remove IntoProtoResult trait in favor of Into<ProtoResult>
seblund Mar 9, 2023
f1de065
Update proto names and add BinaryOp type to binary op types
seblund Mar 18, 2023
ba0583e
Clock reduction fix (#151)
t-lohse Mar 30, 2023
26a5efd
Minor fix for the DummyEdge (#159)
t-lohse Apr 2, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .gitmodules
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
[submodule "Ecdar-ProtoBuf"]
path = Ecdar-ProtoBuf
url = ../Ecdar-ProtoBuf.git
url = https://github.com/Ecdar/Ecdar-ProtoBuf.git
branch = futureproof2
2 changes: 1 addition & 1 deletion Ecdar-ProtoBuf
Submodule Ecdar-ProtoBuf updated 2 files
+52 −17 objects.proto
+131 −45 query.proto
4 changes: 3 additions & 1 deletion benches/simulation_bench.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,15 @@ fn create_step_request(
last_response: &SimulationStartRequest,
) -> SimulationStepRequest {
let cache = ModelCache::default();
helper::create_step_request(
helper::create_step_requests(
component_names,
components_path,
composition,
ConcreteEcdarBackend::handle_start_simulation(last_response.clone(), cache)
.map(Response::new),
)
.next()
.unwrap()
}

fn start_simulation(c: &mut Criterion, id: &str, request: SimulationStartRequest) {
Expand Down
1 change: 0 additions & 1 deletion benches/threadpool_bench.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,6 @@ fn create_query_request(json: &[String], query: &str, hash: u32) -> Request<Quer
components: create_components(json),
components_hash: hash,
}),
ignored_input_outputs: None,
settings: None,
})
}
Expand Down
2 changes: 1 addition & 1 deletion samples/json/Actions/Components/CorrectComponent.json
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
{
"name": "Researcher",
"name": "CorrectComponent",
"declarations": "clock x;",
"locations": [
{
Expand Down
2 changes: 1 addition & 1 deletion samples/json/Actions/Components/NonConsistent.json
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
{
"name": "notConsistent",
"name": "NonConsistent",
"declarations": "clock u;",
"locations": [
{
Expand Down
2 changes: 1 addition & 1 deletion samples/json/Actions/Components/NonDeterministic1.json
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
{
"name": "NonDeterminismCom",
"name": "NonDeterministic1",
"declarations": "",
"locations": [
{
Expand Down
2 changes: 1 addition & 1 deletion samples/json/Actions/Components/NonDeterministic2.json
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
{
"name": "Component2",
"name": "NonDeterministic2",
"declarations": "",
"locations": [
{
Expand Down
3 changes: 3 additions & 0 deletions src/DataReader/component_loader.rs
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,7 @@ pub struct ComponentContainer {
impl ComponentLoader for ComponentContainer {
fn get_component(&mut self, component_name: &str) -> &Component {
if let Some(component) = self.loaded_components.get(component_name) {
assert_eq!(component_name, component.get_name());
component
} else {
panic!("The component '{}' could not be retrieved", component_name);
Expand Down Expand Up @@ -212,6 +213,7 @@ impl ComponentLoader for JsonProjectLoader {
}

if let Some(component) = self.loaded_components.get(component_name) {
assert_eq!(component_name, component.get_name());
component
} else {
panic!("The component '{}' could not be retrieved", component_name);
Expand Down Expand Up @@ -292,6 +294,7 @@ pub struct XmlProjectLoader {
impl ComponentLoader for XmlProjectLoader {
fn get_component(&mut self, component_name: &str) -> &Component {
if let Some(component) = self.loaded_components.get(component_name) {
assert_eq!(component_name, component.get_name());
component
} else {
panic!("The component '{}' could not be retrieved", component_name);
Expand Down
1 change: 0 additions & 1 deletion src/DataReader/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,5 @@ pub mod parse_edge;
pub mod parse_invariant;
pub mod parse_queries;
pub mod proto_reader;
pub mod proto_writer;
pub mod serialization;
pub mod xml_parser;
2 changes: 1 addition & 1 deletion src/DataReader/parse_edge.rs
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ impl Update {
}
}

pub fn parse(edge_attribute_str: &str) -> Result<EdgeAttribute, Error<Rule>> {
pub fn parse(edge_attribute_str: &str) -> Result<EdgeAttribute, Box<Error<Rule>>> {
let mut pairs = EdgeParser::parse(Rule::edgeAttribute, edge_attribute_str)
.unwrap_or_else(|e| panic!("Could not parse as rule with error: {}", e));
let pair = pairs.next().unwrap();
Expand Down
2 changes: 1 addition & 1 deletion src/DataReader/parse_invariant.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use pest::Parser;
#[grammar = "DataReader/grammars/invariant_grammar.pest"]
pub struct InvariantParser;

pub fn parse(edge_attribute_str: &str) -> Result<BoolExpression, Error<Rule>> {
pub fn parse(edge_attribute_str: &str) -> Result<BoolExpression, Box<Error<Rule>>> {
let mut pairs = InvariantParser::parse(Rule::invariant, edge_attribute_str)
.unwrap_or_else(|e| panic!("Could not parse as rule with error: {}", e));
let pair = pairs.next().unwrap();
Expand Down
Loading