Better documentation, formatting code to 80 char
This commit is contained in:
@ -1,26 +1,16 @@
|
|||||||
use std::collections::{BTreeSet, HashMap};
|
use std::collections::{BTreeSet, HashMap};
|
||||||
|
|
||||||
use petgraph::visit::{ EdgeIndexable,
|
use petgraph::visit::{ EdgeRef,
|
||||||
EdgeRef,
|
GraphBase,
|
||||||
IntoEdgeReferences,
|
IntoEdgeReferences,
|
||||||
IntoEdges,
|
IntoEdges,
|
||||||
IntoNodeReferences,
|
IntoNodeReferences };
|
||||||
NodeIndexable };
|
|
||||||
|
|
||||||
struct GraphPartition<'a, G>
|
|
||||||
where
|
|
||||||
G: EdgeIndexable + NodeIndexable + IntoEdgeReferences + IntoNodeReferences
|
|
||||||
+ IntoEdges,
|
|
||||||
G::NodeId: std::cmp::Eq + std::hash::Hash,
|
|
||||||
{
|
|
||||||
pub node_to_block: HashMap<(usize, G::NodeId), u32>,
|
|
||||||
pub block_to_node: HashMap<u32, Vec<(usize, G::NodeId)>>,
|
|
||||||
pub graphs: [&'a G; 2],
|
|
||||||
last_block: u32,
|
|
||||||
blocks: BTreeSet<u32>
|
|
||||||
}
|
|
||||||
|
|
||||||
|
// -----------------------------------------------------------------------------
|
||||||
|
// Helper Functions
|
||||||
|
// -----------------------------------------------------------------------------
|
||||||
|
|
||||||
|
#[inline(always)]
|
||||||
fn equal_vectors<T>(a: &Vec<T>, b: &Vec<T>) -> bool
|
fn equal_vectors<T>(a: &Vec<T>, b: &Vec<T>) -> bool
|
||||||
where
|
where
|
||||||
T: PartialEq
|
T: PartialEq
|
||||||
@ -39,11 +29,27 @@ where
|
|||||||
true
|
true
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
// -----------------------------------------------------------------------------
|
||||||
|
// Bisimilarity
|
||||||
|
// -----------------------------------------------------------------------------
|
||||||
|
|
||||||
|
struct GraphPartition<'a, G>
|
||||||
|
where
|
||||||
|
G: GraphBase,
|
||||||
|
G::NodeId: std::cmp::Eq + std::hash::Hash,
|
||||||
|
{
|
||||||
|
pub node_to_block: HashMap<(usize, G::NodeId), u32>,
|
||||||
|
pub block_to_node: HashMap<u32, Vec<(usize, G::NodeId)>>,
|
||||||
|
pub graphs: [&'a G; 2],
|
||||||
|
last_block: u32,
|
||||||
|
blocks: BTreeSet<u32>
|
||||||
|
}
|
||||||
|
|
||||||
impl<'a, G> GraphPartition<'a, G>
|
impl<'a, G> GraphPartition<'a, G>
|
||||||
where
|
where
|
||||||
G: EdgeIndexable + NodeIndexable + IntoEdgeReferences + IntoNodeReferences
|
G: GraphBase,
|
||||||
+ IntoEdges,
|
G::NodeId: std::cmp::Eq + std::hash::Hash
|
||||||
G::NodeId: std::cmp::Eq + std::hash::Hash,
|
|
||||||
{
|
{
|
||||||
pub fn new(graph_a: &'a G, graph_b: &'a G) -> Self {
|
pub fn new(graph_a: &'a G, graph_b: &'a G) -> Self {
|
||||||
GraphPartition { node_to_block: HashMap::new(),
|
GraphPartition { node_to_block: HashMap::new(),
|
||||||
@ -63,6 +69,7 @@ where
|
|||||||
self.blocks.insert(self.last_block);
|
self.blocks.insert(self.last_block);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[inline(always)]
|
||||||
pub fn iterate_blocks(&self) -> Vec<u32> {
|
pub fn iterate_blocks(&self) -> Vec<u32> {
|
||||||
self.blocks.iter().cloned().collect::<Vec<_>>()
|
self.blocks.iter().cloned().collect::<Vec<_>>()
|
||||||
}
|
}
|
||||||
@ -78,7 +85,13 @@ where
|
|||||||
}
|
}
|
||||||
true
|
true
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl<'a, G> GraphPartition<'a, G>
|
||||||
|
where
|
||||||
|
G: IntoEdges,
|
||||||
|
G::NodeId: std::cmp::Eq + std::hash::Hash,
|
||||||
|
{
|
||||||
fn reachable_blocks(
|
fn reachable_blocks(
|
||||||
&self,
|
&self,
|
||||||
label: &G::EdgeRef,
|
label: &G::EdgeRef,
|
||||||
@ -145,8 +158,7 @@ pub fn bisimilarity_kanellakis_smolka<'a, G>(
|
|||||||
graph_b: &'a G
|
graph_b: &'a G
|
||||||
) -> bool
|
) -> bool
|
||||||
where
|
where
|
||||||
G: EdgeIndexable + NodeIndexable + IntoEdgeReferences + IntoNodeReferences
|
G: IntoNodeReferences + IntoEdges,
|
||||||
+ IntoEdges,
|
|
||||||
G::NodeId: std::cmp::Eq + std::hash::Hash,
|
G::NodeId: std::cmp::Eq + std::hash::Hash,
|
||||||
G::EdgeRef: PartialEq
|
G::EdgeRef: PartialEq
|
||||||
{
|
{
|
||||||
|
|||||||
@ -516,8 +516,6 @@ pub fn bisimilar(
|
|||||||
system_b: String
|
system_b: String
|
||||||
) -> Result<String, String>
|
) -> Result<String, String>
|
||||||
{
|
{
|
||||||
digraph(system_a)?;
|
|
||||||
|
|
||||||
let system_b = read_file(system_a.get_translator(),
|
let system_b = read_file(system_a.get_translator(),
|
||||||
system_b.to_string(),
|
system_b.to_string(),
|
||||||
parser_instructions)?;
|
parser_instructions)?;
|
||||||
@ -529,15 +527,17 @@ pub fn bisimilar(
|
|||||||
EvaluatedSystem::Graph { graph, translator } => {
|
EvaluatedSystem::Graph { graph, translator } => {
|
||||||
if translator != *system_a.get_translator() {
|
if translator != *system_a.get_translator() {
|
||||||
return Err("Bisimilarity not implemented for systems with \
|
return Err("Bisimilarity not implemented for systems with \
|
||||||
different encodings. Serialize the systems with \
|
different encodings. Serialize the systems \
|
||||||
the same translator.".into());
|
with the same translator.".into());
|
||||||
}
|
}
|
||||||
EvaluatedSystem::Graph { graph, translator }
|
EvaluatedSystem::Graph { graph, translator }
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
digraph(system_a)?;
|
||||||
digraph(&mut system_b)?;
|
digraph(&mut system_b)?;
|
||||||
|
|
||||||
|
// since we ran digraph on both they have to be graphs
|
||||||
match (system_a, &system_b) {
|
match (system_a, &system_b) {
|
||||||
(EvaluatedSystem::Graph { graph: a, translator: _ },
|
(EvaluatedSystem::Graph { graph: a, translator: _ },
|
||||||
EvaluatedSystem::Graph { graph: b, translator: _ }) => {
|
EvaluatedSystem::Graph { graph: b, translator: _ }) => {
|
||||||
@ -545,7 +545,10 @@ pub fn bisimilar(
|
|||||||
// and not &mut graph::RSgraph
|
// and not &mut graph::RSgraph
|
||||||
let a: &graph::RSgraph = a;
|
let a: &graph::RSgraph = a;
|
||||||
let b: &graph::RSgraph = b;
|
let b: &graph::RSgraph = b;
|
||||||
Ok(format!("{}", super::bisimilarity::bisimilarity_kanellakis_smolka(&a, &b)))
|
Ok(format!(
|
||||||
|
"{}",
|
||||||
|
super::bisimilarity::bisimilarity_kanellakis_smolka(&a, &b)
|
||||||
|
))
|
||||||
},
|
},
|
||||||
_ => { unreachable!() }
|
_ => { unreachable!() }
|
||||||
}
|
}
|
||||||
@ -565,7 +568,8 @@ fn generate_node_pringting_fn<'a>(
|
|||||||
// We are iterating over the node_display and constructing a function
|
// We are iterating over the node_display and constructing a function
|
||||||
// (accumulator) that prints out our formatted nodes. So at each step we
|
// (accumulator) that prints out our formatted nodes. So at each step we
|
||||||
// call the previous function and add the next string or function.
|
// call the previous function and add the next string or function.
|
||||||
let mut accumulator: Box<dyn Fn(petgraph::prelude::NodeIndex, &RSsystem) -> String> =
|
let mut accumulator:
|
||||||
|
Box<dyn Fn(petgraph::prelude::NodeIndex, &RSsystem) -> String> =
|
||||||
Box::new(|_, _| String::new());
|
Box::new(|_, _| String::new());
|
||||||
for nd in node_display {
|
for nd in node_display {
|
||||||
accumulator = match nd {
|
accumulator = match nd {
|
||||||
@ -575,7 +579,8 @@ fn generate_node_pringting_fn<'a>(
|
|||||||
let val = translator.clone();
|
let val = translator.clone();
|
||||||
Box::new(move |i, n| {
|
Box::new(move |i, n| {
|
||||||
(accumulator)(i, n)
|
(accumulator)(i, n)
|
||||||
+ &graph::GraphMapNodesTy::from(d.clone(), val.clone()).get()(i, n)
|
+ &graph::GraphMapNodesTy::from(d.clone(),
|
||||||
|
val.clone()).get()(i, n)
|
||||||
})
|
})
|
||||||
},
|
},
|
||||||
NodeDisplay::Separator(s) => {
|
NodeDisplay::Separator(s) => {
|
||||||
@ -628,7 +633,8 @@ fn generate_edge_pringting_fn<'a>(
|
|||||||
// We are iterating over the edge_display and constructing a function
|
// We are iterating over the edge_display and constructing a function
|
||||||
// (accumulator) that prints out our formatted nodes. So at each step we
|
// (accumulator) that prints out our formatted nodes. So at each step we
|
||||||
// call the previous function and add the next string or function.
|
// call the previous function and add the next string or function.
|
||||||
let mut accumulator: Box<dyn Fn(petgraph::prelude::EdgeIndex, &RSlabel) -> String> =
|
let mut accumulator:
|
||||||
|
Box<dyn Fn(petgraph::prelude::EdgeIndex, &RSlabel) -> String> =
|
||||||
Box::new(|_, _| String::new());
|
Box::new(|_, _| String::new());
|
||||||
for nd in edge_display {
|
for nd in edge_display {
|
||||||
accumulator = match nd {
|
accumulator = match nd {
|
||||||
@ -638,7 +644,8 @@ fn generate_edge_pringting_fn<'a>(
|
|||||||
let val = translator.clone();
|
let val = translator.clone();
|
||||||
Box::new(move |i, n| {
|
Box::new(move |i, n| {
|
||||||
(accumulator)(i, n)
|
(accumulator)(i, n)
|
||||||
+ &graph::GraphMapEdgesTy::from(d.clone(), val.clone()).get()(i, n)
|
+ &graph::GraphMapEdgesTy::from(d.clone(),
|
||||||
|
val.clone()).get()(i, n)
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
EdgeDisplay::Separator(s) => {
|
EdgeDisplay::Separator(s) => {
|
||||||
@ -656,7 +663,11 @@ fn generate_node_color_fn<'a>(
|
|||||||
node_color: &'a graph::NodeColor,
|
node_color: &'a graph::NodeColor,
|
||||||
original_graph: Rc<graph::RSgraph>,
|
original_graph: Rc<graph::RSgraph>,
|
||||||
translator: Rc<Translator>,
|
translator: Rc<Translator>,
|
||||||
) -> Box<dyn Fn(&Graph<String, String>, <&Graph<String, String, petgraph::Directed, u32> as IntoNodeReferences>::NodeRef) -> String + 'a> {
|
) -> Box<dyn Fn(
|
||||||
|
&Graph<String, String>,
|
||||||
|
<&Graph<String, String, petgraph::Directed, u32> as IntoNodeReferences>::NodeRef
|
||||||
|
) -> String + 'a>
|
||||||
|
{
|
||||||
Box::new(
|
Box::new(
|
||||||
move |i, n| {
|
move |i, n| {
|
||||||
let cloned_node_color = node_color.clone();
|
let cloned_node_color = node_color.clone();
|
||||||
@ -680,7 +691,11 @@ use petgraph::visit::IntoEdgeReferences;
|
|||||||
fn generate_edge_color_fn<'a>(
|
fn generate_edge_color_fn<'a>(
|
||||||
edge_color: &'a graph::EdgeColor,
|
edge_color: &'a graph::EdgeColor,
|
||||||
original_graph: Rc<Graph<RSsystem, RSlabel>>,
|
original_graph: Rc<Graph<RSsystem, RSlabel>>,
|
||||||
) -> Box<dyn Fn(&Graph<String, String>, <&Graph<String, String, petgraph::Directed, u32> as IntoEdgeReferences>::EdgeRef) -> String + 'a> {
|
) -> Box<dyn Fn(
|
||||||
|
&Graph<String, String>,
|
||||||
|
<&Graph<String, String, petgraph::Directed, u32> as IntoEdgeReferences>::EdgeRef
|
||||||
|
) -> String + 'a>
|
||||||
|
{
|
||||||
Box::new(
|
Box::new(
|
||||||
move |i, n| {
|
move |i, n| {
|
||||||
let cloned_edge_color = edge_color.clone();
|
let cloned_edge_color = edge_color.clone();
|
||||||
@ -727,7 +742,9 @@ pub fn dot(
|
|||||||
let graph = Rc::new(graph.to_owned());
|
let graph = Rc::new(graph.to_owned());
|
||||||
|
|
||||||
let node_formatter =
|
let node_formatter =
|
||||||
generate_node_color_fn(node_color, Rc::clone(&graph), rc_translator);
|
generate_node_color_fn(node_color,
|
||||||
|
Rc::clone(&graph),
|
||||||
|
rc_translator);
|
||||||
let edge_formatter =
|
let edge_formatter =
|
||||||
generate_edge_color_fn(edge_color, graph);
|
generate_edge_color_fn(edge_color, graph);
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user