From 567850f0138d98726a72d428219f69103ef1b716 Mon Sep 17 00:00:00 2001 From: elvis Date: Wed, 16 Jul 2025 18:03:31 +0200 Subject: [PATCH] Documentation and better support for deserialization in bisimilarity --- src/rsprocess/presets.rs | 35 ++++++++++++++++++++++++++--------- src/rsprocess/translator.rs | 13 +++++++++++++ 2 files changed, 39 insertions(+), 9 deletions(-) diff --git a/src/rsprocess/presets.rs b/src/rsprocess/presets.rs index 70a3542..73eb9ed 100644 --- a/src/rsprocess/presets.rs +++ b/src/rsprocess/presets.rs @@ -23,6 +23,7 @@ use super::*; // Structures // ----------------------------------------------------------------------------- +/// Describes how the result of some computation has to be saved. pub struct SaveOptions { pub print: bool, pub save: Option>, @@ -58,6 +59,7 @@ impl Default for SaveOptions { } } +/// Describes display options for nodes (RSsystem). #[derive(Clone)] pub enum NodeDisplay { Separator(String), @@ -66,13 +68,14 @@ pub enum NodeDisplay { MaskUncommonEntities(RSset) } - +// Describes display options for edges (RSlabels). #[derive(Clone)] pub enum EdgeDisplay { Separator(String), Display(graph::GraphMapEdges), } +// Describes output options for a graph. pub enum GraphSaveOptions { Dot { node_display: Vec, @@ -91,6 +94,7 @@ pub enum GraphSaveOptions { }, } +/// Describes the computation to apply to the input system or graph. pub enum Instruction { Stats { so: SaveOptions }, Target { so: SaveOptions }, @@ -103,12 +107,14 @@ pub enum Instruction { Bisimilarity { system_b: String, so: SaveOptions } } +/// Describes a system or a graph. pub enum System { Deserialize { path: String }, RSsystem { sys: RSsystem }, } impl System { + /// Deserialize the graph if applicable. pub fn compute( &self, translator: Translator @@ -151,6 +157,7 @@ impl EvaluatedSystem { } } +/// Holds all the computations to be done on the system pub struct Instructions { pub system: System, pub instructions: Vec, @@ -217,8 +224,11 @@ where } => { let mut err = format!( "Unrecognized token \"{t}\" \ - between positions {l} and {r}. Expected: " + between positions {l} and {r}." ); + + // Temporary debug. + err.push_str("Expected: "); let mut it = expected.iter().peekable(); while let Some(s) = it.next() { err.push('('); @@ -500,6 +510,7 @@ pub fn digraph(system: &mut EvaluatedSystem) -> Result<(), String> { Ok(()) } +/// Computes bisimularity of two provided systems pub fn bisimilar( system_a: &mut EvaluatedSystem, system_b: String @@ -511,13 +522,19 @@ pub fn bisimilar( 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() }; + let mut system_b = + match system_b.system.compute(system_a.get_translator().clone())? { + EvaluatedSystem::System { sys, translator } => + EvaluatedSystem::System { sys, translator }, + EvaluatedSystem::Graph { graph, translator } => { + if translator != *system_a.get_translator() { + return Err("Bisimilarity not implemented for systems with \ + different encodings. Serialize the systems with \ + the same translator.".into()); + } + EvaluatedSystem::Graph { graph, translator } + } + }; digraph(&mut system_b)?; diff --git a/src/rsprocess/translator.rs b/src/rsprocess/translator.rs index 71f643f..ee0548d 100644 --- a/src/rsprocess/translator.rs +++ b/src/rsprocess/translator.rs @@ -33,6 +33,19 @@ impl Default for Translator { } } +impl PartialEq for Translator { + fn eq(&self, other: &Self) -> bool { + for (s, id) in self.strings.iter() { + match other.strings.get(s) { + None => return false, + Some(id2) if id != id2 => return false, + _ => {} + } + } + true + } +} + impl Translator { /// converts a string into an id pub fn encode(&mut self, s: impl Into) -> IdType {