diff --git a/assert/src/dsl.rs b/assert/src/dsl.rs index c40c54f..b5ec0f6 100644 --- a/assert/src/dsl.rs +++ b/assert/src/dsl.rs @@ -1,8 +1,8 @@ use std::collections::HashMap; -use serde::{Serialize, Deserialize}; use rsprocess::set::BasicSet; use rsprocess::{element, graph, label, process, set, system, translator}; +use serde::{Deserialize, Serialize}; /// If changing IntegerType in assert.rs, also change from Num to another /// similar parser with different return type in grammar.lalrpop in @@ -196,7 +196,9 @@ pub enum AssertReturnValue { impl Default for Assert { fn default() -> Self { - Self { tree: Tree::Return(Box::new(Expression::True)) } + Self { + tree: Tree::Return(Box::new(Expression::True)), + } } } diff --git a/assert/src/rsassert.rs b/assert/src/rsassert.rs index d9d0d1d..c4ef645 100644 --- a/assert/src/rsassert.rs +++ b/assert/src/rsassert.rs @@ -1,8 +1,8 @@ use std::collections::HashMap; -use serde::{Serialize, Deserialize}; use rsprocess::translator::PrintableWithTranslator; use rsprocess::{graph, label, set, system, translator}; +use serde::{Deserialize, Serialize}; use super::dsl::*; diff --git a/execution/src/presets.rs b/execution/src/presets.rs index 9d364ec..6ed6f1c 100644 --- a/execution/src/presets.rs +++ b/execution/src/presets.rs @@ -737,9 +737,9 @@ where .map_edges(edge_relabeler, &mut system_a.translator)?; let b: Graph = system_b - .graph - .unwrap() - .map_edges(edge_relabeler, &mut system_b.translator)?; + .graph + .unwrap() + .map_edges(edge_relabeler, &mut system_b.translator)?; Ok(format!( "{}", // bisimilarity::bisimilarity_kanellakis_smolka::bisimilarity(&&a, &&b) diff --git a/grammar_separated/src/grammar.lalrpop b/grammar_separated/src/grammar.lalrpop index b31cecd..0d0afde 100644 --- a/grammar_separated/src/grammar.lalrpop +++ b/grammar_separated/src/grammar.lalrpop @@ -2,12 +2,9 @@ use std::rc::Rc; use std::str::FromStr; use lalrpop_util::ParseError; -// use assert::{relabel, grouping}; use rsprocess::{set, reaction, process, environment, system, label}; -use rsprocess::element::IdType; +use rsprocess::element::{self, IdType}; use rsprocess::translator::Translator; -// use execution::presets; -// use rsprocess::graph; use crate::custom_error; grammar(translator: &mut Translator); @@ -197,6 +194,16 @@ pub Set: set::Set = { .collect::>()) }; +pub PositiveSet: set::PositiveSet = { + > => + set::PositiveSet::from(s) +}; + +PositiveLiteral: (element::IdType, element::IdState) = { + "+" => (translator.encode(t), element::IdState::Positive), + "-" => (translator.encode(t), element::IdState::Negative), +} + // ----------------------------------------------------------------------------- // ReactionParser diff --git a/rsprocess/src/environment.rs b/rsprocess/src/environment.rs index b26681b..1e9c597 100644 --- a/rsprocess/src/environment.rs +++ b/rsprocess/src/environment.rs @@ -452,7 +452,6 @@ impl From> for Environment { } } - // ----------------------------------------------------------------------------- // Confluence // ----------------------------------------------------------------------------- diff --git a/rsprocess/src/system.rs b/rsprocess/src/system.rs index f78b697..40c5e6c 100644 --- a/rsprocess/src/system.rs +++ b/rsprocess/src/system.rs @@ -105,6 +105,11 @@ pub trait ExtensionsSystem: BasicSystem { fn slice_trace( &self, ) -> Result, String>; + + fn slice_trace_limit( + &self, + limit: usize, + ) -> Result, String>; } impl ExtensionsSystem for T { @@ -363,6 +368,62 @@ impl ExtensionsSystem for T { // trace.enabled_reactions.pop(); Ok(trace) } + + #[allow(clippy::field_reassign_with_default)] + #[allow(clippy::type_complexity)] + fn slice_trace_limit( + &self, + limit: usize, + ) -> Result, String> { + let mut trace = SlicingTrace::default(); + + trace.context_elements = Rc::new(self.context_elements()); + trace.products_elements = Rc::new(self.products_elements()); + trace.reactions = Rc::new(self.reactions().clone()); + trace.systems.push(Rc::new(self.clone())); + trace.elements.push(SlicingElement::from(( + Self::Set::default(), + self.available_entities().clone(), + ))); + + let current: Option<(Self::Set, Self::Set, Vec, Self)> = + self.to_slicing_iterator()?.next(); + if current.is_none() { + return Ok(trace); + } + let current = current.unwrap(); + + let (context, products, enabled_reactions, mut current) = current; + trace + .elements + .push(SlicingElement::from((context, products))); + trace + .enabled_reactions + .push(EnabledReactions::from(enabled_reactions)); + trace.systems.push(Rc::new(current.clone())); + + let mut n = limit; + loop { + n -= 1; + let t = current.to_slicing_iterator()?.next(); + if let Some((context, products, enabled_reactions, next_sys)) = t + && n > 0 + { + current = next_sys; + trace + .elements + .push(SlicingElement::from((context, products))); + trace + .enabled_reactions + .push(EnabledReactions::from(enabled_reactions)); + trace.systems.push(Rc::new(current.clone())); + } else { + break; + } + } + // trace.enabled_reactions.pop(); + Ok(trace) + } } // ----------------------------------------------------------------------------- @@ -508,7 +569,7 @@ impl BasicSystem for System { fn to_slicing_iterator( &self, ) -> Result, String> { - unimplemented!() + TraceIterator::::try_from(self) } fn environment(&self) -> &Self::Environment { diff --git a/rsprocess/src/trace.rs b/rsprocess/src/trace.rs index a7ea637..9cb6347 100644 --- a/rsprocess/src/trace.rs +++ b/rsprocess/src/trace.rs @@ -192,10 +192,8 @@ impl EnabledReactions { } } - #[derive(Clone, Debug, Hash, Serialize, Deserialize)] -pub struct SlicingTrace -{ +pub struct SlicingTrace { pub elements: Vec>, pub enabled_reactions: Vec, @@ -411,14 +409,14 @@ impl< if elements.peek().is_some() { writeln!( f, - "{}\n\t|\n{: ^17}\n\t|\n\t▼", + "{}\n\t\t|\n{: ^17}\n\t\t|\n\t\tv", Formatter::from(translator, el), format!("({})", Formatter::from(translator, r)), )?; } else { writeln!( f, - "{}\n\t|\n{: ^17}\n\t|\n\t?", + "{}\n\t\t|\n{: ^17}\n\t\t|\n\t\t?", Formatter::from(translator, el), format!("({})", Formatter::from(translator, r)), )?; @@ -426,7 +424,7 @@ impl< } else if elements.peek().is_some() { writeln!( f, - "{}\n\t|\n\t|\n\t|\n\t▼", + "{}\n\t\t|\n\t\t|\n\t\t|\n\t\tv", Formatter::from(translator, el) )?; } else { diff --git a/rsprocess/src/transitions.rs b/rsprocess/src/transitions.rs index bd9df6c..c305e47 100644 --- a/rsprocess/src/transitions.rs +++ b/rsprocess/src/transitions.rs @@ -225,11 +225,56 @@ impl<'a> TryFrom<&'a PositiveSystem> } } +impl<'a> TryFrom<&'a System> for TraceIterator<'a, Set, System, Process> { + type Error = String; + + fn try_from(value: &'a System) -> Result { + match value.unfold() { + | Ok(o) => Ok(Self { + choices_iterator: o.into_iter(), + system: value, + }), + | Err(e) => Err(e), + } + } +} + impl<'a> Iterator for TraceIterator<'a, Set, System, Process> { type Item = (Set, Set, Vec, System); fn next(&mut self) -> Option { - unimplemented!() + let (context, k) = self.choices_iterator.next()?; + let total_entities = + self.system.available_entities().union(context.as_ref()); + + let (enabled_reaction_positions, all_products) = + self.system.reactions().iter().enumerate().fold( + (vec![], Set::default()), + |mut acc, (pos, reaction)| { + if reaction.enabled(&total_entities) { + acc.0.push(pos); + (acc.0, acc.1.union(&reaction.products)) + } else { + acc + } + }, + ); + + let new_system = System::from( + Rc::clone(&self.system.delta), + // all_products.add_unique(&self.system. + // negated_products_elements()), + all_products.clone(), + (*k).clone(), + Rc::clone(&self.system.reaction_rules), + ); + + Some(( + context.as_ref().clone(), + all_products, + enabled_reaction_positions, + new_system, + )) } }