2025-11-16 02:07:47 +01:00
|
|
|
use super::kanellakis_smolka::bisimilarity;
|
2025-08-23 23:40:19 +02:00
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn identity_kanellakis_smolka() {
|
|
|
|
|
use petgraph::Graph;
|
|
|
|
|
let mut graph_a = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_a_1 = graph_a.add_node(1);
|
|
|
|
|
let node_a_2 = graph_a.add_node(2);
|
|
|
|
|
graph_a.add_edge(node_a_1, node_a_2, 1);
|
|
|
|
|
|
|
|
|
|
assert!(bisimilarity(&&graph_a, &&graph_a))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn identity_kanellakis_smolka_2() {
|
|
|
|
|
use petgraph::Graph;
|
|
|
|
|
let mut graph_a = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_a_1 = graph_a.add_node(1);
|
|
|
|
|
let node_a_2 = graph_a.add_node(2);
|
|
|
|
|
graph_a.add_edge(node_a_1, node_a_2, 1);
|
|
|
|
|
let node_a_3 = graph_a.add_node(3);
|
|
|
|
|
graph_a.add_edge(node_a_1, node_a_3, 1);
|
|
|
|
|
let node_a_6 = graph_a.add_node(6);
|
|
|
|
|
graph_a.add_edge(node_a_2, node_a_6, 2);
|
|
|
|
|
let node_a_4 = graph_a.add_node(4);
|
|
|
|
|
graph_a.add_edge(node_a_3, node_a_4, 2);
|
|
|
|
|
let node_a_7 = graph_a.add_node(7);
|
|
|
|
|
graph_a.add_edge(node_a_6, node_a_7, 2);
|
|
|
|
|
let node_a_5 = graph_a.add_node(5);
|
|
|
|
|
graph_a.add_edge(node_a_4, node_a_5, 2);
|
|
|
|
|
let node_a_8 = graph_a.add_node(8);
|
|
|
|
|
graph_a.add_edge(node_a_7, node_a_8, 3);
|
|
|
|
|
graph_a.add_edge(node_a_8, node_a_7, 3);
|
|
|
|
|
graph_a.add_edge(node_a_8, node_a_8, 3);
|
|
|
|
|
|
|
|
|
|
assert!(bisimilarity(&&graph_a, &&graph_a))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn identity_different_weights_kanellakis_smolka() {
|
|
|
|
|
use petgraph::Graph;
|
|
|
|
|
let mut graph_a = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_a_1 = graph_a.add_node(1);
|
|
|
|
|
let node_a_2 = graph_a.add_node(2);
|
|
|
|
|
graph_a.add_edge(node_a_1, node_a_2, 1);
|
|
|
|
|
|
|
|
|
|
let mut graph_b = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_b_1 = graph_b.add_node(1);
|
|
|
|
|
let node_b_2 = graph_b.add_node(2);
|
|
|
|
|
graph_b.add_edge(node_b_1, node_b_2, 2);
|
|
|
|
|
|
|
|
|
|
assert!(!bisimilarity(&&graph_a, &&graph_b))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn not_bisimilar_kanellakis_smolka() {
|
|
|
|
|
use petgraph::Graph;
|
|
|
|
|
let mut graph_a = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_a_1 = graph_a.add_node(1);
|
|
|
|
|
let node_a_2 = graph_a.add_node(2);
|
|
|
|
|
graph_a.add_edge(node_a_1, node_a_2, 1);
|
|
|
|
|
|
|
|
|
|
let mut graph_b = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_b_1 = graph_b.add_node(1);
|
|
|
|
|
let node_b_2 = graph_b.add_node(2);
|
|
|
|
|
graph_b.add_edge(node_b_1, node_b_2, 1);
|
|
|
|
|
let node_b_3 = graph_b.add_node(3);
|
|
|
|
|
graph_b.add_edge(node_b_1, node_b_3, 2);
|
|
|
|
|
|
|
|
|
|
assert!(!bisimilarity(&&graph_a, &&graph_b))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn not_bisimilar_kanellakis_smolka_2() {
|
|
|
|
|
use petgraph::Graph;
|
|
|
|
|
let mut graph_a = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_a_1 = graph_a.add_node(1);
|
|
|
|
|
let node_a_2 = graph_a.add_node(2);
|
|
|
|
|
graph_a.add_edge(node_a_1, node_a_2, 1);
|
|
|
|
|
let node_a_3 = graph_a.add_node(3);
|
|
|
|
|
graph_a.add_edge(node_a_1, node_a_3, 1);
|
|
|
|
|
let node_a_6 = graph_a.add_node(6);
|
|
|
|
|
graph_a.add_edge(node_a_2, node_a_6, 2);
|
|
|
|
|
let node_a_4 = graph_a.add_node(4);
|
|
|
|
|
graph_a.add_edge(node_a_3, node_a_4, 2);
|
|
|
|
|
let node_a_7 = graph_a.add_node(7);
|
|
|
|
|
graph_a.add_edge(node_a_6, node_a_7, 2);
|
|
|
|
|
let node_a_5 = graph_a.add_node(5);
|
|
|
|
|
graph_a.add_edge(node_a_4, node_a_5, 2);
|
|
|
|
|
let node_a_8 = graph_a.add_node(8);
|
|
|
|
|
graph_a.add_edge(node_a_7, node_a_8, 3);
|
|
|
|
|
graph_a.add_edge(node_a_8, node_a_7, 3);
|
|
|
|
|
graph_a.add_edge(node_a_8, node_a_8, 3);
|
|
|
|
|
|
|
|
|
|
let mut graph_b = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_b_1 = graph_b.add_node(1);
|
|
|
|
|
let node_b_2 = graph_b.add_node(2);
|
|
|
|
|
graph_b.add_edge(node_b_1, node_b_2, 1);
|
|
|
|
|
let node_b_3 = graph_b.add_node(3);
|
|
|
|
|
graph_b.add_edge(node_b_2, node_b_3, 2);
|
|
|
|
|
let node_b_4 = graph_b.add_node(4);
|
|
|
|
|
graph_b.add_edge(node_b_3, node_b_4, 2);
|
|
|
|
|
|
|
|
|
|
assert!(!bisimilarity(&&graph_a, &&graph_b))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn not_bisimilar_kanellakis_smolka_3() {
|
|
|
|
|
use petgraph::Graph;
|
|
|
|
|
let mut graph_b = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_b_1 = graph_b.add_node(1);
|
|
|
|
|
let node_b_2 = graph_b.add_node(2);
|
|
|
|
|
graph_b.add_edge(node_b_1, node_b_2, 1);
|
|
|
|
|
let node_b_3 = graph_b.add_node(3);
|
|
|
|
|
graph_b.add_edge(node_b_2, node_b_3, 2);
|
|
|
|
|
let node_b_4 = graph_b.add_node(4);
|
|
|
|
|
graph_b.add_edge(node_b_3, node_b_4, 2);
|
|
|
|
|
|
|
|
|
|
let mut graph_c = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_c_1 = graph_c.add_node(1);
|
|
|
|
|
let node_c_2 = graph_c.add_node(2);
|
|
|
|
|
graph_c.add_edge(node_c_1, node_c_2, 1);
|
|
|
|
|
let node_c_3 = graph_c.add_node(3);
|
|
|
|
|
graph_c.add_edge(node_c_1, node_c_3, 2);
|
|
|
|
|
graph_c.add_edge(node_c_2, node_c_3, 2);
|
|
|
|
|
|
|
|
|
|
assert!(!bisimilarity(&&graph_b, &&graph_c))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn bisimilar_kanellakis_smolka() {
|
|
|
|
|
use petgraph::Graph;
|
|
|
|
|
let mut graph_b = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_b_1 = graph_b.add_node(1);
|
|
|
|
|
let node_b_2 = graph_b.add_node(2);
|
|
|
|
|
graph_b.add_edge(node_b_1, node_b_2, 1);
|
|
|
|
|
let node_b_3 = graph_b.add_node(3);
|
|
|
|
|
graph_b.add_edge(node_b_2, node_b_3, 2);
|
|
|
|
|
let node_b_4 = graph_b.add_node(4);
|
|
|
|
|
graph_b.add_edge(node_b_3, node_b_4, 2);
|
|
|
|
|
|
|
|
|
|
let mut graph_c = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_c_1 = graph_c.add_node(1);
|
|
|
|
|
let node_c_2 = graph_c.add_node(2);
|
|
|
|
|
graph_c.add_edge(node_c_1, node_c_2, 1);
|
|
|
|
|
let node_c_3 = graph_c.add_node(3);
|
|
|
|
|
graph_c.add_edge(node_c_2, node_c_3, 2);
|
|
|
|
|
let node_c_4 = graph_c.add_node(4);
|
|
|
|
|
graph_c.add_edge(node_c_3, node_c_4, 2);
|
|
|
|
|
let node_c_5 = graph_c.add_node(5);
|
|
|
|
|
graph_c.add_edge(node_c_1, node_c_5, 1);
|
|
|
|
|
let node_c_6 = graph_c.add_node(6);
|
|
|
|
|
graph_c.add_edge(node_c_5, node_c_6, 2);
|
|
|
|
|
let node_c_7 = graph_c.add_node(7);
|
|
|
|
|
graph_c.add_edge(node_c_6, node_c_7, 2);
|
|
|
|
|
|
|
|
|
|
assert!(bisimilarity(&&graph_b, &&graph_c))
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#[test]
|
|
|
|
|
fn bisimilar_kanellakis_smolka_2() {
|
|
|
|
|
use petgraph::Graph;
|
|
|
|
|
let mut graph_a = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_a_1 = graph_a.add_node(1);
|
|
|
|
|
let node_a_2 = graph_a.add_node(2);
|
|
|
|
|
graph_a.add_edge(node_a_1, node_a_2, 1);
|
|
|
|
|
let node_a_3 = graph_a.add_node(3);
|
|
|
|
|
graph_a.add_edge(node_a_1, node_a_3, 1);
|
|
|
|
|
graph_a.add_edge(node_a_2, node_a_3, 2);
|
|
|
|
|
graph_a.add_edge(node_a_3, node_a_3, 2);
|
|
|
|
|
|
|
|
|
|
let mut graph_b = Graph::new();
|
|
|
|
|
|
|
|
|
|
let node_b_1 = graph_b.add_node(1);
|
|
|
|
|
let node_b_2 = graph_b.add_node(2);
|
|
|
|
|
graph_b.add_edge(node_b_1, node_b_2, 1);
|
|
|
|
|
graph_b.add_edge(node_b_2, node_b_2, 2);
|
|
|
|
|
|
|
|
|
|
assert!(bisimilarity(&&graph_a, &&graph_b))
|
|
|
|
|
}
|