Skip to content

Commit

Permalink
Diabled CR for reachability queries. To avoid test issues in two cases
Browse files Browse the repository at this point in the history
  • Loading branch information
SilverBrother committed Nov 27, 2023
1 parent 500c548 commit 08bc6e0
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 10 deletions.
14 changes: 5 additions & 9 deletions src/model_objects/component.rs
Original file line number Diff line number Diff line change
Expand Up @@ -202,24 +202,23 @@ impl Component {
let mut equivalent_clock_groups: Vec<HashSet<String>> = vec![used_clocks.clone()];

Check warning on line 202 in src/model_objects/component.rs

View workflow job for this annotation

GitHub Actions / cargo fmt

Diff in /home/runner/work/Reveaal/Reveaal/src/model_objects/component.rs

for edge in &self.edges {
let local_equivalences = self.find_local_equivalences(edge);
let local_equivalences = self.find_local_equivalences(edge).expect("Could not find local equivalences");
self.update_global_groups(&mut equivalent_clock_groups, &local_equivalences);
}
equivalent_clock_groups
}
fn find_local_equivalences(&self, edge: &Edge) -> HashMap<String, u32> {
fn find_local_equivalences(&self, edge: &Edge) -> Result<HashMap<String, u32>, String> {
let mut local_equivalence_map = HashMap::new();
match &edge.update.clone() {
Some(updates) => {
for update in updates {
local_equivalence_map.insert(update.variable.clone(), update.expression.get_evaluated_int().unwrap() as u32);
local_equivalence_map.insert(update.variable.clone(), update.expression.get_evaluated_int()? as u32);
}
}
None => {}
}
local_equivalence_map
Ok(local_equivalence_map)
}
//New Commit

fn update_global_groups(
&self,
Expand Down Expand Up @@ -528,10 +527,7 @@ mod tests{

}

fn test_get_or_insert<>(){

}

#[test]
fn test_compress_dcls(){

}
Expand Down
20 changes: 19 additions & 1 deletion src/tests/refinement/helper.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,9 @@ use crate::data_reader::component_loader::{JsonProjectLoader, XmlProjectLoader};
use crate::data_reader::parse_queries;
use crate::extract_system_rep::ExecutableQueryError;
use crate::logging::setup_logger;
use crate::model_objects::expressions::QueryExpression;
use crate::model_objects::Query;
use crate::parse_queries::Rule::reachability;

Check warning on line 7 in src/tests/refinement/helper.rs

View workflow job for this annotation

GitHub Actions / Tests Ubuntu

unused import: `crate::parse_queries::Rule::reachability`

Check warning on line 7 in src/tests/refinement/helper.rs

View workflow job for this annotation

GitHub Actions / Build Ubuntu

unused import: `crate::parse_queries::Rule::reachability`

Check warning on line 7 in src/tests/refinement/helper.rs

View workflow job for this annotation

GitHub Actions / Build Windows

unused import: `crate::parse_queries::Rule::reachability`

Check warning on line 7 in src/tests/refinement/helper.rs

View workflow job for this annotation

GitHub Actions / Build MacOS

unused import: `crate::parse_queries::Rule::reachability`
use crate::system::extract_system_rep::create_executable_query;
use crate::system::query_failures::QueryResult;
use crate::transition_systems::transition_system::component_loader_to_transition_system;
Expand Down Expand Up @@ -63,7 +65,23 @@ pub fn json_run_query(path: &str, query: &str) -> Result<QueryResult, Executable
};
// After implementing clock reduction on component level, a few tests are failing due to
// inconsistencies with initial state and global clock. Turn boolean true to ignore inconsistencies
project_loader.get_settings_mut().disable_clock_reduction = true;
if let Some(query_type) = q.get_query() {
match query_type {
QueryExpression::Reachability{ .. } => {
project_loader.get_settings_mut().disable_clock_reduction = true;
}
, QueryExpression::Refinement(_,_)
| QueryExpression::Consistency(_)
| QueryExpression::Implementation(_)
| QueryExpression::Determinism(_)
| QueryExpression::Specification(_)
| QueryExpression::BisimMinim(_)
| QueryExpression::GetComponent(_)
| QueryExpression::Prune(_) => {
project_loader.get_settings_mut().disable_clock_reduction = false;
},
}
}

let mut comp_loader = project_loader.to_comp_loader();
let query = create_executable_query(&q, &mut *comp_loader)?;
Expand Down

0 comments on commit 08bc6e0

Please sign in to comment.