From 27ce4899ca63e3db4862cbd6e1f5553478c112f7 Mon Sep 17 00:00:00 2001 From: elvis Date: Sun, 22 Jun 2025 16:09:31 +0200 Subject: [PATCH] Confluence module --- src/rsprocess/confluence.rs | 76 ++++++++++ src/rsprocess/mod.rs | 1 + src/rsprocess/perpetual.rs | 275 ++++++++++++++++++++++++++++++------ 3 files changed, 310 insertions(+), 42 deletions(-) create mode 100644 src/rsprocess/confluence.rs diff --git a/src/rsprocess/confluence.rs b/src/rsprocess/confluence.rs new file mode 100644 index 0000000..3909df0 --- /dev/null +++ b/src/rsprocess/confluence.rs @@ -0,0 +1,76 @@ +#![allow(dead_code)] + +use super::perpetual::{ + lollipops_only_loop_decomposed, + lollipops_only_loop_decomposed_named, + lollipops_prefix_len_loop_decomposed, + lollipops_prefix_len_loop_decomposed_named}; +use super::structure::{RSenvironment, RSreaction, RSset}; +use super::translator::IdType; +use std::cmp; + +pub fn confluent( + delta: &RSenvironment, + reaction_rules: &[RSreaction], + entities: &[RSset], +) -> Option<(usize, usize, Vec)> { + let mut max_distance = 0; + let mut dimension = 0; + let mut hoop = vec![]; + + if let Some(el) = entities.first() { + if let Some(new_hoop) = lollipops_only_loop_decomposed(delta, reaction_rules, el).first() { + dimension = new_hoop.len(); + hoop = new_hoop.clone(); + } + } + + for available_entities in entities.iter().skip(1) { + // FIXME we take just the first? do we compare all? + if let Some((prefix_len, new_hoop)) = + lollipops_prefix_len_loop_decomposed(delta, reaction_rules, available_entities).first() + { + if hoop.len() != dimension || hoop != *new_hoop { + return None; + } + max_distance = cmp::max(max_distance, *prefix_len); + } else { + return None; + } + } + Some((max_distance, dimension, hoop)) +} + + +pub fn confluent_named( + delta: &RSenvironment, + reaction_rules: &[RSreaction], + entities: &[RSset], + symb: IdType +) -> Option<(usize, usize, Vec)> { + let mut max_distance = 0; + let mut dimension = 0; + let mut hoop = vec![]; + + if let Some(el) = entities.first() { + if let Some(new_hoop) = lollipops_only_loop_decomposed_named(delta, reaction_rules, el, symb) { + dimension = new_hoop.len(); + hoop = new_hoop.clone(); + } + } + + for available_entities in entities.iter().skip(1) { + // FIXME we take just the first? do we compare all? + if let Some((prefix_len, new_hoop)) = + lollipops_prefix_len_loop_decomposed_named(delta, reaction_rules, available_entities, symb) + { + if hoop.len() != dimension || hoop != *new_hoop { + return None; + } + max_distance = cmp::max(max_distance, prefix_len); + } else { + return None; + } + } + Some((max_distance, dimension, hoop)) +} diff --git a/src/rsprocess/mod.rs b/src/rsprocess/mod.rs index ce489ff..4ffb7a3 100644 --- a/src/rsprocess/mod.rs +++ b/src/rsprocess/mod.rs @@ -4,3 +4,4 @@ pub mod support_structures; pub mod classical; pub mod transitions; pub mod perpetual; +pub mod confluence; diff --git a/src/rsprocess/perpetual.rs b/src/rsprocess/perpetual.rs index 4e3d051..23a9ca4 100644 --- a/src/rsprocess/perpetual.rs +++ b/src/rsprocess/perpetual.rs @@ -3,7 +3,77 @@ use std::rc::Rc; use super::classical::compute_all_owned; use super::translator::IdType; -use super::structure::{RSsystem, RSprocess, RSset, RSreaction}; +use super::structure::{RSenvironment, RSprocess, RSreaction, RSset, RSsystem}; + + +// returns the prefix and the loop from a trace +fn split<'a>( + set: &'a RSset, + trace: &'a [RSset] +) -> Option<(&'a[RSset], &'a[RSset])> { + let position = trace.iter().rposition(|x| x == set); + position.map(|pos| trace.split_at(pos)) +} + +// finds the loops by simulating the system +fn find_loop( + rs: &[RSreaction], + entities: RSset, + q: &RSset +) -> (Vec, Vec) { + let mut entities = entities; + let mut trace = vec![]; + loop { + if let Some((prefix, hoop)) = split(&entities, &trace) { + return (prefix.to_vec(), hoop.to_vec()); + } else { + let t = entities.union(q); + let products = compute_all_owned(&t, rs); + trace.push(entities.clone()); + entities = products; + } + } +} + + +// finds the loops by simulating the system +fn find_only_loop(rs: &[RSreaction], entities: RSset, q: &RSset) -> Vec { + let mut entities = entities; + let mut trace = vec![]; + loop { + if let Some((_prefix, hoop)) = split(&entities, &trace) { + return hoop.to_vec(); + } else { + let t = entities.union(q); + let products = compute_all_owned(&t, rs); + trace.push(entities.clone()); + entities = products; + } + } +} + + +// finds the loops and the length of the prefix by simulating the system +fn find_prefix_len_loop( + rs: &[RSreaction], + entities: RSset, + q: &RSset +) -> (usize, Vec) { + let mut entities = entities; + let mut trace = vec![]; + loop { + if let Some((prefix, hoop)) = split(&entities, &trace) { + return (prefix.len(), hoop.to_vec()); + } else { + let t = entities.union(q); + let products = compute_all_owned(&t, rs); + trace.push(entities.clone()); + entities = products; + } + } +} + +// ----------------------------------------------------------------------------- // finds only the rules X = pre(Q, rec(X)), but not only x = pre(Q, rec(x)) // to use in filter_map @@ -23,57 +93,32 @@ fn filter_delta<'a>(x: (&IdType, &'a RSprocess)) -> Option<&'a RSset> { } } -// returns the prefix and the loop from a trace -fn split<'a>(set: &'a RSset, trace: &'a [RSset]) -> Option<(&'a[RSset], &'a[RSset])> { - let position = trace.iter().rposition(|x| x == set); - position.map(|pos| trace.split_at(pos)) -} - -// finds the loops by simulating the system -fn find_loop(rs: &Rc>, entities: RSset, q: &RSset) -> (Vec, Vec) { - let mut entities = entities; - let mut trace = vec![]; - loop { - if let Some((prefix, hoop)) = split(&entities, &trace) { - return (prefix.to_vec(), hoop.to_vec()); - } else { - let t = entities.union(q); - let products = compute_all_owned(&t, rs); - trace.push(entities.clone()); - entities = products; - } - } -} - -// finds the loops by simulating the system -fn find_only_loop(rs: &Rc>, entities: RSset, q: &RSset) -> Vec { - let mut entities = entities; - let mut trace = vec![]; - loop { - if let Some((_prefix, hoop)) = split(&entities, &trace) { - return hoop.to_vec(); - } else { - let t = entities.union(q); - let products = compute_all_owned(&t, rs); - trace.push(entities.clone()); - entities = products; - } - } -} // see lollipop -pub fn lollipops(system: RSsystem) -> Vec<(Vec, Vec)> { +pub fn lollipops_decomposed( + delta: &RSenvironment, + reaction_rules: &[RSreaction], + available_entities: &RSset +) -> Vec<(Vec, Vec)> { // FIXME: i think we are only interested in "x", not all symbols that // satisfy X = pre(Q, rec(X)) - let filtered = system.get_delta().iter().filter_map(filter_delta); + let filtered = delta.iter().filter_map(filter_delta); - let find_loop_fn = |q| find_loop(system.get_reaction_rules(), - system.get_available_entities().clone(), + let find_loop_fn = |q| find_loop(reaction_rules, + available_entities.clone(), q); filtered.map(find_loop_fn).collect::>() } +// see lollipop +pub fn lollipops(system: RSsystem) -> Vec<(Vec, Vec)> { + lollipops_decomposed(system.get_delta(), + system.get_reaction_rules(), + system.get_available_entities()) +} + +// see loop pub fn lollipops_only_loop(system: RSsystem) -> Vec> { // FIXME: i think we are only interested in "x", not all symbols that // satisfy X = pre(Q, rec(X)) @@ -85,3 +130,149 @@ pub fn lollipops_only_loop(system: RSsystem) -> Vec> { filtered.map(find_loop_fn).collect::>() } + + +pub fn lollipops_prefix_len_loop_decomposed( + delta: &RSenvironment, + reaction_rules: &[RSreaction], + available_entities: &RSset +) -> Vec<(usize, Vec)> { + // FIXME: i think we are only interested in "x", not all symbols that + // satisfy X = pre(Q, rec(X)) + let filtered = delta.iter().filter_map(filter_delta); + + let find_loop_fn = |q| find_prefix_len_loop(reaction_rules, + available_entities.clone(), + q); + + filtered.map(find_loop_fn).collect::>() +} + +// see loop +pub fn lollipops_only_loop_decomposed( + delta: &RSenvironment, + reaction_rules: &[RSreaction], + available_entities: &RSset +) -> Vec> { + // FIXME: i think we are only interested in "x", not all symbols that + // satisfy X = pre(Q, rec(X)) + let filtered = delta.iter().filter_map(filter_delta); + + let find_loop_fn = |q| find_only_loop(reaction_rules, + available_entities.clone(), + q); + + filtered.map(find_loop_fn).collect::>() +} + +// ----------------------------------------------------------------------------- +// Named versions +// ----------------------------------------------------------------------------- + +// finds only the rules symb = pre(Q, rec(symb)), get symb from a translator +// to use in filter_map +fn filter_delta_named<'a>( + x: (&IdType, &'a RSprocess), + symb: &IdType +) -> Option<&'a RSset> { + use super::structure::RSprocess::*; + let (id, rest) = x; + if id != symb { + return None; + } + match rest { + EntitySet{ entities, next_process} => { + match &**next_process { + RecursiveIdentifier{ identifier } if identifier == id => { + Some(entities) + }, + _ => None + } + }, + _ => None + } +} + +// see lollipop +pub fn lollipops_decomposed_named( + delta: &RSenvironment, + reaction_rules: &[RSreaction], + available_entities: &RSset, + symb: IdType +) -> Option<(Vec, Vec)> { + // FIXME: i think we are only interested in "x", not all symbols that + // satisfy X = pre(Q, rec(X)) + let filtered = delta.iter().filter_map(|x| filter_delta_named(x, &symb)).next(); + + let find_loop_fn = |q| find_loop(reaction_rules, + available_entities.clone(), + q); + + filtered.map(find_loop_fn) +} + +// see lollipop +pub fn lollipops_named( + system: RSsystem, + symb: IdType +) -> Option<(Vec, Vec)> { + lollipops_decomposed_named(system.get_delta(), + system.get_reaction_rules(), + system.get_available_entities(), + symb) +} + +// see loop +pub fn lollipops_only_loop_named( + system: RSsystem, + symb: IdType +) -> Option> { + // FIXME: i think we are only interested in "x", not all symbols that + // satisfy X = pre(Q, rec(X)) + let filtered = system.get_delta().iter() + .filter_map(|x| filter_delta_named(x, &symb)).next(); + + let find_loop_fn = + |q| find_only_loop(system.get_reaction_rules(), + system.get_available_entities().clone(), + q); + + filtered.map(find_loop_fn) +} + +pub fn lollipops_prefix_len_loop_decomposed_named( + delta: &RSenvironment, + reaction_rules: &[RSreaction], + available_entities: &RSset, + symb: IdType +) -> Option<(usize, Vec)> { + // FIXME: i think we are only interested in "x", not all symbols that + // satisfy X = pre(Q, rec(X)) + let filtered = delta.iter() + .filter_map(|x| filter_delta_named(x, &symb)).next(); + + let find_loop_fn = |q| find_prefix_len_loop(reaction_rules, + available_entities.clone(), + q); + + filtered.map(find_loop_fn) +} + +// see loop +pub fn lollipops_only_loop_decomposed_named( + delta: &RSenvironment, + reaction_rules: &[RSreaction], + available_entities: &RSset, + symb: IdType +) -> Option> { + // FIXME: i think we are only interested in "x", not all symbols that + // satisfy X = pre(Q, rec(X)) + let filtered = delta.iter() + .filter_map(|x| filter_delta_named(x, &symb)).next(); + + let find_loop_fn = |q| find_only_loop(reaction_rules, + available_entities.clone(), + q); + + filtered.map(find_loop_fn) +}