Skip to content

Commit

Permalink
Unify the 'display' format and 'parse' format for HctlTreeNode
Browse files Browse the repository at this point in the history
  • Loading branch information
@ondrej33
ondrej33 committed Dec 23, 2023
1 parent d317d2a commit f785844
Show file tree
Hide file tree
Showing 8 changed files with 135 additions and 170 deletions.
10 changes: 2 additions & 8 deletions src/analysis.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,18 +38,12 @@ pub fn analyse_formulae(
for (i, formula) in formulae.iter().enumerate() {
print_if_allowed(format!("Original formula n.{}: {formula}", i + 1), print_op);
let tree = parse_hctl_formula(formula.as_str())?;
print_if_allowed(
format!("Parsed version: {}", tree.subform_str),
print_op,
);
print_if_allowed(format!("Parsed version: {tree}"), print_op);

let modified_tree =
check_props_and_rename_vars(tree, HashMap::new(), String::new(), &plain_context)?;
let num_hctl_vars = collect_unique_hctl_vars(modified_tree.clone()).len();
print_if_allowed(
format!("Modified version: {}", modified_tree.subform_str),
print_op,
);
print_if_allowed(format!("Modified version: {modified_tree}"), print_op);
print_if_allowed("-----".to_string(), print_op);

parsed_trees.push(modified_tree);
Expand Down
34 changes: 17 additions & 17 deletions src/evaluation/algorithm.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ pub fn eval_node(
let mut save_to_cache = false;

// get canonized form of this sub-formula, and mapping of how vars are canonized
let (canonized_form, renaming) = get_canonical_and_mapping(node.subform_str.clone());
let (canonized_form, renaming) = get_canonical_and_mapping(node.to_string());

if eval_info.duplicates.contains_key(canonized_form.as_str()) {
if eval_info.cache.contains_key(canonized_form.as_str()) {
Expand Down Expand Up @@ -94,30 +94,30 @@ pub fn eval_node(
},
NodeType::UnaryNode(op, child) => match op {
UnaryOp::Not => eval_neg(graph, &eval_node(*child, graph, eval_info, steady_states)),
UnaryOp::Ex => eval_ex(
UnaryOp::EX => eval_ex(
graph,
&eval_node(*child, graph, eval_info, steady_states),
steady_states,
),
UnaryOp::Ax => eval_ax(
UnaryOp::AX => eval_ax(
graph,
&eval_node(*child, graph, eval_info, steady_states),
steady_states,
),
UnaryOp::Ef => {
UnaryOp::EF => {
eval_ef_saturated(graph, &eval_node(*child, graph, eval_info, steady_states))
}
UnaryOp::Af => eval_af(
UnaryOp::AF => eval_af(
graph,
&eval_node(*child, graph, eval_info, steady_states),
steady_states,
),
UnaryOp::Eg => eval_eg(
UnaryOp::EG => eval_eg(
graph,
&eval_node(*child, graph, eval_info, steady_states),
steady_states,
),
UnaryOp::Ag => eval_ag(graph, &eval_node(*child, graph, eval_info, steady_states)),
UnaryOp::AG => eval_ag(graph, &eval_node(*child, graph, eval_info, steady_states)),
},
NodeType::BinaryNode(op, left, right) => {
match op {
Expand All @@ -140,24 +140,24 @@ pub fn eval_node(
&eval_node(*left, graph, eval_info, steady_states),
&eval_node(*right, graph, eval_info, steady_states),
),
BinaryOp::Eu => eval_eu_saturated(
BinaryOp::EU => eval_eu_saturated(
graph,
&eval_node(*left, graph, eval_info, steady_states),
&eval_node(*right, graph, eval_info, steady_states),
),
BinaryOp::Au => eval_au(
BinaryOp::AU => eval_au(
graph,
&eval_node(*left, graph, eval_info, steady_states),
&eval_node(*right, graph, eval_info, steady_states),
steady_states,
),
BinaryOp::Ew => eval_ew(
BinaryOp::EW => eval_ew(
graph,
&eval_node(*left, graph, eval_info, steady_states),
&eval_node(*right, graph, eval_info, steady_states),
steady_states,
),
BinaryOp::Aw => eval_aw(
BinaryOp::AW => eval_aw(
graph,
&eval_node(*left, graph, eval_info, steady_states),
&eval_node(*right, graph, eval_info, steady_states),
Expand Down Expand Up @@ -202,8 +202,8 @@ pub fn eval_node(
fn is_attractor_pattern(node: HctlTreeNode) -> bool {
match node.node_type {
NodeType::HybridNode(HybridOp::Bind, var1, child1) => match child1.node_type {
NodeType::UnaryNode(UnaryOp::Ag, child2) => match child2.node_type {
NodeType::UnaryNode(UnaryOp::Ef, child3) => match child3.node_type {
NodeType::UnaryNode(UnaryOp::AG, child2) => match child2.node_type {
NodeType::UnaryNode(UnaryOp::EF, child3) => match child3.node_type {
NodeType::TerminalNode(Atomic::Var(var2)) => var1 == var2,
_ => false,
},
Expand All @@ -220,7 +220,7 @@ fn is_attractor_pattern(node: HctlTreeNode) -> bool {
fn is_fixed_point_pattern(node: HctlTreeNode) -> bool {
match node.node_type {
NodeType::HybridNode(HybridOp::Bind, var1, child1) => match child1.node_type {
NodeType::UnaryNode(UnaryOp::Ax, child2) => match child2.node_type {
NodeType::UnaryNode(UnaryOp::AX, child2) => match child2.node_type {
NodeType::TerminalNode(Atomic::Var(var2)) => var1 == var2,
_ => false,
},
Expand Down Expand Up @@ -272,7 +272,7 @@ mod tests {
/// Test recognition of fixed-point pattern.
fn test_fixed_point_pattern() {
let tree = HctlTreeNode::mk_hybrid_node(
HctlTreeNode::mk_unary_node(HctlTreeNode::mk_var_node("x".to_string()), UnaryOp::Ax),
HctlTreeNode::mk_unary_node(HctlTreeNode::mk_var_node("x".to_string()), UnaryOp::AX),
"x".to_string(),
HybridOp::Bind,
);
Expand All @@ -286,9 +286,9 @@ mod tests {
HctlTreeNode::mk_unary_node(
HctlTreeNode::mk_unary_node(
HctlTreeNode::mk_var_node("x".to_string()),
UnaryOp::Ef,
UnaryOp::EF,
),
UnaryOp::Ag,
UnaryOp::AG,
),
"x".to_string(),
HybridOp::Bind,
Expand Down
2 changes: 1 addition & 1 deletion src/evaluation/eval_context.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ mod tests {
let formula = "!{x}: (AX {x} & AX {x})";
let syntax_tree = parse_hctl_formula(formula).unwrap();

let expected_duplicates = HashMap::from([("(Ax {var0})".to_string(), 1)]);
let expected_duplicates = HashMap::from([("(AX {var0})".to_string(), 1)]);
let eval_info = EvalContext::new(expected_duplicates.clone());

assert_eq!(eval_info, EvalContext::from_single_tree(&syntax_tree));
Expand Down
87 changes: 7 additions & 80 deletions src/evaluation/mark_duplicate_subform.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ pub fn mark_duplicates_canonized_multiple(root_nodes: &Vec<HctlTreeNode>) -> Has

let mut skip = false;
let (current_subform_canonical, renaming) =
get_canonical_and_mapping(current_node.subform_str.clone());
get_canonical_and_mapping(current_node.to_string());

// only mark duplicates with at max 1 variable (to not cause var name collisions during caching)
// todo: extend this for any number of variables
Expand Down Expand Up @@ -78,7 +78,7 @@ pub fn mark_duplicates_canonized_multiple(root_nodes: &Vec<HctlTreeNode>) -> Has
// we continue with node from lower level, so we empty the set of nodes to compare
last_height = current_node.height;
same_height_canonical_strings.clear();
same_height_canonical_strings.insert(get_canonical(current_node.subform_str.clone()));
same_height_canonical_strings.insert(get_canonical(current_node.to_string()));
}

// add children of current node to the heap_queue
Expand All @@ -104,79 +104,6 @@ pub fn mark_duplicates_canonized_single(root_node: &HctlTreeNode) -> HashMap<Str
mark_duplicates_canonized_multiple(&vec![root_node.clone()])
}

/*
/// DEPRECATED VERSION THAT DOES NOT UTILIZE CANONIZATION, USE THE VERSION ABOVE
/// Check if there are some duplicate subtrees in the given syntax tree
/// Save the (raw) duplicate sub-formulae + the number of their appearances
/// This version does not consider canonical forms! - only recognizes fully identical duplicates
/// Note that terminal nodes (props, vars, constants) are not considered
pub fn mark_duplicates_deprecated(root_node: &HctlTreeNode) -> HashMap<String, i32> {
// go through the nodes from top, use height to compare only those with the same level
// once we find duplicate, do not continue traversing its branch (it will be skipped during eval)
let mut duplicates: HashMap<String, i32> = HashMap::new();
let mut heap_queue: BinaryHeap<&HctlTreeNode> = BinaryHeap::new();
let mut last_height = root_node.height.clone();
let mut same_height_node_strings: HashSet<String> = HashSet::new();
heap_queue.push(root_node);
// because we are traversing a tree, we dont care about cycles
while let Some(current_node) = heap_queue.pop() {
//println!("{}", current_node.subform_str.as_str());
// lets stop the process when we hit the first terminal node
// terminals are not worth to mark as duplicates and use them for caching
if current_node.height == 0 {
break;
}
let mut skip = false;
if last_height == current_node.height {
// if we have saved some nodes of the same height, compare them with the current one
for other_node_string in same_height_node_strings.clone() {
if other_node_string == current_node.subform_str.as_str() {
if duplicates.contains_key(current_node.subform_str.as_str()) {
duplicates
.insert(current_node.subform_str.clone(), duplicates[&current_node.subform_str] + 1);
} else {
duplicates.insert(current_node.subform_str.clone(), 1);
}
skip = true; // skip the descendants of the duplicate current_node
break;
}
}
// do not traverse subtree of the duplicate later (will be cached during eval)
if skip {
continue;
}
same_height_node_strings.insert(current_node.subform_str.clone());
} else {
// we got node from lower level, so we empty the set of nodes to compare
last_height = current_node.height;
same_height_node_strings.clear();
same_height_node_strings.insert(current_node.subform_str.clone());
}
// add children of current_node to the heap_queue
match &current_node.node_type {
NodeType::TerminalNode(_) => {}
NodeType::UnaryNode(_, child) => {
heap_queue.push(child);
}
NodeType::BinaryNode(_, left, right) => {
heap_queue.push(left);
heap_queue.push(right);
}
NodeType::HybridNode(_, _, child) => {
heap_queue.push(child);
}
}
}
duplicates
}
*/

#[cfg(test)]
mod tests {
use crate::evaluation::mark_duplicate_subform::{
Expand All @@ -193,7 +120,7 @@ mod tests {
/// Compare automatically detected duplicate sub-formulae to expected ones.
fn test_duplicates_single_simple() {
let formula = "!{x}: 3{y}: (AX {x} & AX {y})";
let expected_duplicates = HashMap::from([("(Ax {var0})".to_string(), 1)]);
let expected_duplicates = HashMap::from([("(AX {var0})".to_string(), 1)]);

// define any placeholder bn
let bn = BooleanNetwork::try_from_bnet("v1, v1").unwrap();
Expand All @@ -210,8 +137,8 @@ mod tests {
fn test_duplicates_single_complex() {
let formula = "(!{x}: 3{y}: ((AG EF {x} & AG EF {y}) & (EF {y}))) & (!{z}: EF {z})";
let expected_duplicates = HashMap::from([
("(Ag (Ef {var0}))".to_string(), 1),
("(Ef {var0})".to_string(), 2),
("(AG (EF {var0}))".to_string(), 1),
("(EF {var0})".to_string(), 2),
]);

// define any placeholder bn
Expand All @@ -233,8 +160,8 @@ mod tests {
"!{z}: AX {z}",
];
let expected_duplicates = HashMap::from([
("(Ax {var0})".to_string(), 2),
("(Bind {var0}: (Ax {var0}))".to_string(), 1),
("(AX {var0})".to_string(), 2),
("(!{var0}: (AX {var0}))".to_string(), 1),
]);

// define any placeholder bn
Expand Down
36 changes: 24 additions & 12 deletions src/preprocessing/node.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ pub enum NodeType {
/// Structure for a HCTL formula syntax tree.
#[derive(Clone, Debug, Eq, Hash, PartialEq)]
pub struct HctlTreeNode {
pub subform_str: String,
pub formula_str: String,
pub height: i32,
pub node_type: NodeType,
}
Expand Down Expand Up @@ -51,6 +51,7 @@ impl Ord for HctlTreeNode {
}
}

/// Generating new instances of `HctlTreeNode`.
impl HctlTreeNode {
/// Parse `tokens` of HCTL formula into an abstract syntax tree using recursive steps.
/// It is recommended to not use this method for parsing, but rather choose from functions
Expand All @@ -62,16 +63,21 @@ impl HctlTreeNode {
/// Create a hybrid node from given arguments.
pub fn mk_hybrid_node(child: HctlTreeNode, var: String, op: HybridOp) -> HctlTreeNode {
HctlTreeNode {
subform_str: format!("({} {{{}}}: {})", op, var, child.subform_str),
formula_str: format!("({op}{{{var}}}: {child})"),
height: child.height + 1,
node_type: NodeType::HybridNode(op, var, Box::new(child)),
}
}

/// Create an unary node from given arguments.
pub fn mk_unary_node(child: HctlTreeNode, op: UnaryOp) -> HctlTreeNode {
let subform_str = if matches!(op, UnaryOp::Not) {
format!("({op}{child})")
} else {
format!("({op} {child})")
};
HctlTreeNode {
subform_str: format!("({} {})", op, child.subform_str),
formula_str: subform_str,
height: child.height + 1,
node_type: NodeType::UnaryNode(op, Box::new(child)),
}
Expand All @@ -80,7 +86,7 @@ impl HctlTreeNode {
/// Create a binary node from given arguments.
pub fn mk_binary_node(left: HctlTreeNode, right: HctlTreeNode, op: BinaryOp) -> HctlTreeNode {
HctlTreeNode {
subform_str: format!("({} {} {})", left.subform_str, op, right.subform_str),
formula_str: format!("({left} {op} {right})"),
height: cmp::max(left.height, right.height) + 1,
node_type: NodeType::BinaryNode(op, Box::new(left), Box::new(right)),
}
Expand All @@ -89,7 +95,7 @@ impl HctlTreeNode {
/// Create a terminal `variable` node from given arguments.
pub fn mk_var_node(var_name: String) -> HctlTreeNode {
HctlTreeNode {
subform_str: format!("{{{var_name}}}"),
formula_str: format!("{{{var_name}}}"),
height: 0,
node_type: NodeType::TerminalNode(Atomic::Var(var_name)),
}
Expand All @@ -98,7 +104,7 @@ impl HctlTreeNode {
/// Create a terminal `proposition` node from given arguments.
pub fn mk_prop_node(prop_name: String) -> HctlTreeNode {
HctlTreeNode {
subform_str: prop_name.clone(),
formula_str: prop_name.clone(),
height: 0,
node_type: NodeType::TerminalNode(Atomic::Prop(prop_name)),
}
Expand All @@ -109,13 +115,13 @@ impl HctlTreeNode {
pub fn mk_constant_node(constant_val: bool) -> HctlTreeNode {
if constant_val {
HctlTreeNode {
subform_str: "True".to_string(),
formula_str: "True".to_string(),
height: 0,
node_type: NodeType::TerminalNode(Atomic::True),
}
} else {
HctlTreeNode {
subform_str: "False".to_string(),
formula_str: "False".to_string(),
height: 0,
node_type: NodeType::TerminalNode(Atomic::False),
}
Expand All @@ -125,16 +131,22 @@ impl HctlTreeNode {
/// Create a terminal `wild-card proposition` node from given arguments.
pub fn mk_wild_card_node(prop_name: String) -> HctlTreeNode {
HctlTreeNode {
subform_str: format!("%{prop_name}%"),
formula_str: format!("%{prop_name}%"),
height: 0,
node_type: NodeType::TerminalNode(Atomic::WildCardProp(prop_name)),
}
}
}

impl HctlTreeNode {
pub fn as_str(&self) -> &str {
self.formula_str.as_str()
}
}

impl fmt::Display for HctlTreeNode {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "{}", self.subform_str)
write!(f, "{}", self.formula_str)
}
}

Expand Down Expand Up @@ -162,8 +174,8 @@ mod tests {
assert!(node2 <= node1);

// test display
let node1_str = "(Bind {x}: (Exists {y}: (Jump {x}: (((~ {y}) & (%subst% & True)) ^ v1))))";
let node2_str = "(Bind {x}: (Ax {x}))";
let node1_str = "(!{x}: (3{y}: (@{x}: (((~{y}) & (%subst% & True)) ^ v1))))";
let node2_str = "(!{x}: (AX {x}))";
assert_eq!(node1.to_string(), node1_str.to_string());
assert_eq!(node2.to_string(), node2_str.to_string());
}
Expand Down
Loading

0 comments on commit f785844

Please sign in to comment.