From fe05ff35f26379b688199dcd28d8ef31129dcf91 Mon Sep 17 00:00:00 2001 From: elvis Date: Wed, 16 Jul 2025 00:05:14 +0200 Subject: [PATCH] Bisimilarity working? --- src/rsprocess/grammar.lalrpop | 8 ++- src/rsprocess/graph.rs | 7 ++- src/rsprocess/mod.rs | 1 + src/rsprocess/presets.rs | 94 +++++++++++++++++++++++++++-------- src/rsprocess/serialize.rs | 11 ++-- src/rsprocess/structure.rs | 2 +- testing/first.system | 8 +-- 7 files changed, 92 insertions(+), 39 deletions(-) diff --git a/src/rsprocess/grammar.lalrpop b/src/rsprocess/grammar.lalrpop index 9cdddbf..97d9dde 100644 --- a/src/rsprocess/grammar.lalrpop +++ b/src/rsprocess/grammar.lalrpop @@ -37,7 +37,7 @@ match { "Print", "Save", "Dot", "GraphML", "Serialize", "Stats", "Target", "Run", "Loop", "Frequency", "LimitFrequency", - "FastFrequency", "Digraph", + "FastFrequency", "Digraph", "Bisimilarity", "Deserialize", "Hide", "Entities", "MaskEntities", "MaskContext", "Products", "MaskProducts", "Union", "MaskUnion", @@ -523,6 +523,8 @@ Instruction: presets::Instruction = { presets::Instruction::FastFrequency { experiment: p, so }, "Digraph" ">" > => presets::Instruction::Digraph { gso }, + "Bisimilarity" "(" ")" ">" => + presets::Instruction::Bisimilarity { system_b: p, so }, } pub Run: presets::Instructions = { @@ -530,6 +532,10 @@ pub Run: presets::Instructions = { Instructions { system: presets::System::RSsystem { sys }, instructions: instr }, + => + Instructions { system: presets::System::RSsystem { sys }, + instructions: vec![] }, + "Deserialize" "(" ")" > => Instructions { system: presets::System::Deserialize { path }, diff --git a/src/rsprocess/graph.rs b/src/rsprocess/graph.rs index 441b4fb..bf51f18 100644 --- a/src/rsprocess/graph.rs +++ b/src/rsprocess/graph.rs @@ -7,7 +7,8 @@ use super::support_structures::TransitionsIterator; use super::translator::{self, IdType}; use std::rc::Rc; -type RSgraph = Graph; + +pub type RSgraph = Graph; /// Creates a graph starting from a system as root node pub fn digraph( @@ -364,7 +365,9 @@ impl GraphMapEdgesTy { // ----------------------------------------------------------------------------- // Formatting Nodes & Edges // ----------------------------------------------------------------------------- -use petgraph::visit::{IntoNodeReferences, IntoEdgeReferences, EdgeRef}; +use petgraph::visit::{ IntoEdgeReferences, + IntoNodeReferences, + EdgeRef }; type RSdotGraph = Graph; type RSformatNodeTy = diff --git a/src/rsprocess/mod.rs b/src/rsprocess/mod.rs index 5c1fe8a..06f3e0a 100644 --- a/src/rsprocess/mod.rs +++ b/src/rsprocess/mod.rs @@ -13,3 +13,4 @@ pub mod graph; pub mod rsdot; pub mod serialize; pub mod presets; +pub mod bisimilarity; diff --git a/src/rsprocess/presets.rs b/src/rsprocess/presets.rs index eb02b73..7a859ae 100644 --- a/src/rsprocess/presets.rs +++ b/src/rsprocess/presets.rs @@ -98,6 +98,7 @@ pub enum Instruction { LimitFrequency { experiment: String, so: SaveOptions }, FastFrequency { experiment: String, so: SaveOptions }, Digraph { gso: Vec }, + Bisimilarity { system_b: String, so: SaveOptions } } pub enum System { @@ -105,17 +106,6 @@ pub enum System { RSsystem { sys: RSsystem }, } -pub enum EvaluatedSystem { - Graph { - graph: Graph, - translator: Translator, - }, - System { - sys: RSsystem, - translator: Translator, - }, -} - impl System { pub fn compute( &self, @@ -135,6 +125,30 @@ impl System { } } +pub enum EvaluatedSystem { + Graph { + graph: graph::RSgraph, + translator: Translator, + }, + System { + sys: RSsystem, + translator: Translator, + }, +} + +impl EvaluatedSystem { + pub fn get_translator(&mut self) -> &mut Translator { + match self { + EvaluatedSystem::Graph { graph: _, translator } => { + translator + }, + EvaluatedSystem::System { sys: _, translator } => { + translator + } + } + } +} + pub struct Instructions { pub system: System, pub instructions: Vec, @@ -474,17 +488,50 @@ pub fn fast_freq( /// Computes the LTS. /// equivalent to main_do(digraph, Arcs) or to main_do(advdigraph, Arcs) pub fn digraph(system: &mut EvaluatedSystem) -> Result<(), String> { - *system = if let EvaluatedSystem::System { sys, translator } = system { - EvaluatedSystem::Graph { - graph: graph::digraph(sys.clone())?, - translator: translator.to_owned(), - } - } else { - return Ok(()); - }; + if let EvaluatedSystem::System { sys, translator } = system { + *system = + EvaluatedSystem::Graph { + graph: graph::digraph(sys.clone())?, + translator: translator.to_owned(), + }; + } Ok(()) } +pub fn bisimilar( + system_a: &mut EvaluatedSystem, + system_b: String +) -> Result +{ + digraph(system_a)?; + + let system_b = read_file(system_a.get_translator(), + system_b.to_string(), + parser_instructions)?; + + let system_b = match system_b.system { + System::RSsystem { sys } => sys, + _ => return Err("Not implemented yet".into()) + }; + + let mut system_b = EvaluatedSystem::System { sys: system_b, + translator: system_a.get_translator().clone() }; + + digraph(&mut system_b)?; + + match (system_a, &system_b) { + (EvaluatedSystem::Graph { graph: a, translator: _ }, + EvaluatedSystem::Graph { graph: b, translator: _ }) => { + // needed because rust cant see that we want to use &graph::RSgraph + // and not &mut graph::RSgraph + let a: &graph::RSgraph = a; + let b: &graph::RSgraph = b; + Ok(format!("{}", super::bisimilarity::bisimilarity_kanellakis_smolka(&a, &b))) + }, + _ => { unreachable!() } + } +} + // ----------------------------------------------------------------------------- // Output Functions // ----------------------------------------------------------------------------- @@ -555,7 +602,7 @@ use petgraph::visit::IntoNodeReferences; #[allow(clippy::type_complexity)] fn generate_node_color_fn<'a>( node_color: &'a graph::NodeColor, - original_graph: Rc>, + original_graph: Rc, translator: Rc, ) -> Box, <&Graph as IntoNodeReferences>::NodeRef) -> String + 'a> { Box::new( @@ -708,8 +755,8 @@ pub fn serialize(system: &EvaluatedSystem, path: String) -> Result<(), String> { /// N.B. graph size in memory might be much larger after serialization and /// deserialization pub fn deserialize( - input_path: String -) -> Result<(Graph, Translator), String> + input_path: String, +) -> Result<(graph::RSgraph, Translator), String> { // relative path let mut path = match env::current_dir() { @@ -802,6 +849,9 @@ fn execute( } } } + Instruction::Bisimilarity { system_b, so } => { + save_options!(bisimilar(system, system_b)?, so); + } } Ok(()) } diff --git a/src/rsprocess/serialize.rs b/src/rsprocess/serialize.rs index 2b99ff7..227485a 100644 --- a/src/rsprocess/serialize.rs +++ b/src/rsprocess/serialize.rs @@ -5,22 +5,21 @@ use std::io; -use petgraph::Graph; use serde::{Deserialize, Serialize}; +use super::graph; -use super::{structure::{RSlabel, RSsystem}, - translator::Translator}; +use super::translator::Translator; #[derive(Serialize, Deserialize)] struct GraphAndTranslator { - graph: Graph, + graph: graph::RSgraph, translator: Translator } /// Serializer for graph and translator. pub fn ser( writer: W, - graph: &Graph, + graph: &graph::RSgraph, translator: &Translator ) -> Result<(), serde_cbor_2::Error> where @@ -36,7 +35,7 @@ where /// Deserializer for file that contains graph and translator. pub fn de( reader: R -) -> Result<(Graph, Translator), serde_cbor_2::Error> +) -> Result<(graph::RSgraph, Translator), serde_cbor_2::Error> where R: io::Read, { diff --git a/src/rsprocess/structure.rs b/src/rsprocess/structure.rs index 1cc4777..bb47399 100644 --- a/src/rsprocess/structure.rs +++ b/src/rsprocess/structure.rs @@ -491,7 +491,7 @@ impl Default for RSsystem { // ----------------------------------------------------------------------------- // RSlabel // ----------------------------------------------------------------------------- -#[derive(Clone, Debug, Serialize, Deserialize)] +#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq, PartialOrd)] pub struct RSlabel { pub available_entities: RSset, pub context: RSset, diff --git a/testing/first.system b/testing/first.system index 561accc..f261659 100644 --- a/testing/first.system +++ b/testing/first.system @@ -4,10 +4,4 @@ Context: [({a,b}.{a}.{a,c}.x + {a,b}.{a}.{a}.nill)] Reactions: ([{a,b}, {c}, {b}]) -Digraph - > Dot - | Context - | Hide - | Context.EntitySet ⊆ {a, c} ? "lightblue" || Context.NonDeterministicChoice ? "yellow" ! "#123" - | Entities < {a} ? "white" ! "#lightgreen" - > Print +Bisimilarity ("testing/adversarial.system") > Print \ No newline at end of file