Bisimilarity working?
This commit is contained in:
@ -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" ">" <gso: Separated_Or<GraphSaveOptions, "|">> =>
|
||||
presets::Instruction::Digraph { gso },
|
||||
"Bisimilarity" "(" <p: Path> ")" ">" <so: SaveOptions> =>
|
||||
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 },
|
||||
|
||||
<sys: System> =>
|
||||
Instructions { system: presets::System::RSsystem { sys },
|
||||
instructions: vec![] },
|
||||
|
||||
"Deserialize" "(" <path: Path> ")"
|
||||
<instr: Separated_Or<Instruction, ",">> =>
|
||||
Instructions { system: presets::System::Deserialize { path },
|
||||
|
||||
@ -7,7 +7,8 @@ use super::support_structures::TransitionsIterator;
|
||||
use super::translator::{self, IdType};
|
||||
use std::rc::Rc;
|
||||
|
||||
type RSgraph = Graph<RSsystem, RSlabel, Directed, u32>;
|
||||
|
||||
pub type RSgraph = Graph<RSsystem, RSlabel, Directed, u32>;
|
||||
|
||||
/// 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<String, String, Directed, u32>;
|
||||
type RSformatNodeTy =
|
||||
|
||||
@ -13,3 +13,4 @@ pub mod graph;
|
||||
pub mod rsdot;
|
||||
pub mod serialize;
|
||||
pub mod presets;
|
||||
pub mod bisimilarity;
|
||||
|
||||
@ -98,6 +98,7 @@ pub enum Instruction {
|
||||
LimitFrequency { experiment: String, so: SaveOptions },
|
||||
FastFrequency { experiment: String, so: SaveOptions },
|
||||
Digraph { gso: Vec<GraphSaveOptions> },
|
||||
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<RSsystem, RSlabel>,
|
||||
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<Instruction>,
|
||||
@ -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<String, String>
|
||||
{
|
||||
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<Graph<RSsystem, RSlabel>>,
|
||||
original_graph: Rc<graph::RSgraph>,
|
||||
translator: Rc<Translator>,
|
||||
) -> Box<dyn Fn(&Graph<String, String>, <&Graph<String, String, petgraph::Directed, u32> 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<RSsystem, RSlabel>, 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(())
|
||||
}
|
||||
|
||||
@ -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<RSsystem, RSlabel>,
|
||||
graph: graph::RSgraph,
|
||||
translator: Translator
|
||||
}
|
||||
|
||||
/// Serializer for graph and translator.
|
||||
pub fn ser<W>(
|
||||
writer: W,
|
||||
graph: &Graph<RSsystem, RSlabel>,
|
||||
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<R>(
|
||||
reader: R
|
||||
) -> Result<(Graph<RSsystem, RSlabel>, Translator), serde_cbor_2::Error>
|
||||
) -> Result<(graph::RSgraph, Translator), serde_cbor_2::Error>
|
||||
where
|
||||
R: io::Read,
|
||||
{
|
||||
|
||||
@ -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,
|
||||
|
||||
Reference in New Issue
Block a user