Documentation and better support for deserialization in bisimilarity
This commit is contained in:
@ -23,6 +23,7 @@ use super::*;
|
|||||||
// Structures
|
// Structures
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
|
|
||||||
|
/// Describes how the result of some computation has to be saved.
|
||||||
pub struct SaveOptions {
|
pub struct SaveOptions {
|
||||||
pub print: bool,
|
pub print: bool,
|
||||||
pub save: Option<Vec<String>>,
|
pub save: Option<Vec<String>>,
|
||||||
@ -58,6 +59,7 @@ impl Default for SaveOptions {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Describes display options for nodes (RSsystem).
|
||||||
#[derive(Clone)]
|
#[derive(Clone)]
|
||||||
pub enum NodeDisplay {
|
pub enum NodeDisplay {
|
||||||
Separator(String),
|
Separator(String),
|
||||||
@ -66,13 +68,14 @@ pub enum NodeDisplay {
|
|||||||
MaskUncommonEntities(RSset)
|
MaskUncommonEntities(RSset)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// Describes display options for edges (RSlabels).
|
||||||
#[derive(Clone)]
|
#[derive(Clone)]
|
||||||
pub enum EdgeDisplay {
|
pub enum EdgeDisplay {
|
||||||
Separator(String),
|
Separator(String),
|
||||||
Display(graph::GraphMapEdges),
|
Display(graph::GraphMapEdges),
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// Describes output options for a graph.
|
||||||
pub enum GraphSaveOptions {
|
pub enum GraphSaveOptions {
|
||||||
Dot {
|
Dot {
|
||||||
node_display: Vec<NodeDisplay>,
|
node_display: Vec<NodeDisplay>,
|
||||||
@ -91,6 +94,7 @@ pub enum GraphSaveOptions {
|
|||||||
},
|
},
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Describes the computation to apply to the input system or graph.
|
||||||
pub enum Instruction {
|
pub enum Instruction {
|
||||||
Stats { so: SaveOptions },
|
Stats { so: SaveOptions },
|
||||||
Target { so: SaveOptions },
|
Target { so: SaveOptions },
|
||||||
@ -103,12 +107,14 @@ pub enum Instruction {
|
|||||||
Bisimilarity { system_b: String, so: SaveOptions }
|
Bisimilarity { system_b: String, so: SaveOptions }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Describes a system or a graph.
|
||||||
pub enum System {
|
pub enum System {
|
||||||
Deserialize { path: String },
|
Deserialize { path: String },
|
||||||
RSsystem { sys: RSsystem },
|
RSsystem { sys: RSsystem },
|
||||||
}
|
}
|
||||||
|
|
||||||
impl System {
|
impl System {
|
||||||
|
/// Deserialize the graph if applicable.
|
||||||
pub fn compute(
|
pub fn compute(
|
||||||
&self,
|
&self,
|
||||||
translator: Translator
|
translator: Translator
|
||||||
@ -151,6 +157,7 @@ impl EvaluatedSystem {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Holds all the computations to be done on the system
|
||||||
pub struct Instructions {
|
pub struct Instructions {
|
||||||
pub system: System,
|
pub system: System,
|
||||||
pub instructions: Vec<Instruction>,
|
pub instructions: Vec<Instruction>,
|
||||||
@ -217,8 +224,11 @@ where
|
|||||||
} => {
|
} => {
|
||||||
let mut err = format!(
|
let mut err = format!(
|
||||||
"Unrecognized token \"{t}\" \
|
"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();
|
let mut it = expected.iter().peekable();
|
||||||
while let Some(s) = it.next() {
|
while let Some(s) = it.next() {
|
||||||
err.push('(');
|
err.push('(');
|
||||||
@ -500,6 +510,7 @@ pub fn digraph(system: &mut EvaluatedSystem) -> Result<(), String> {
|
|||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Computes bisimularity of two provided systems
|
||||||
pub fn bisimilar(
|
pub fn bisimilar(
|
||||||
system_a: &mut EvaluatedSystem,
|
system_a: &mut EvaluatedSystem,
|
||||||
system_b: String
|
system_b: String
|
||||||
@ -511,13 +522,19 @@ pub fn bisimilar(
|
|||||||
system_b.to_string(),
|
system_b.to_string(),
|
||||||
parser_instructions)?;
|
parser_instructions)?;
|
||||||
|
|
||||||
let system_b = match system_b.system {
|
let mut system_b =
|
||||||
System::RSsystem { sys } => sys,
|
match system_b.system.compute(system_a.get_translator().clone())? {
|
||||||
_ => return Err("Not implemented yet".into())
|
EvaluatedSystem::System { sys, translator } =>
|
||||||
};
|
EvaluatedSystem::System { sys, translator },
|
||||||
|
EvaluatedSystem::Graph { graph, translator } => {
|
||||||
let mut system_b = EvaluatedSystem::System { sys: system_b,
|
if translator != *system_a.get_translator() {
|
||||||
translator: system_a.get_translator().clone() };
|
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)?;
|
digraph(&mut system_b)?;
|
||||||
|
|
||||||
|
|||||||
@ -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 {
|
impl Translator {
|
||||||
/// converts a string into an id
|
/// converts a string into an id
|
||||||
pub fn encode(&mut self, s: impl Into<String>) -> IdType {
|
pub fn encode(&mut self, s: impl Into<String>) -> IdType {
|
||||||
|
|||||||
Reference in New Issue
Block a user