diff --git a/src/analysis.rs b/src/analysis.rs index 127f0d5..74d9521 100644 --- a/src/analysis.rs +++ b/src/analysis.rs @@ -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); diff --git a/src/evaluation/algorithm.rs b/src/evaluation/algorithm.rs index 4e756a9..21885a3 100644 --- a/src/evaluation/algorithm.rs +++ b/src/evaluation/algorithm.rs @@ -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()) { @@ -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 { @@ -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), @@ -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, }, @@ -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, }, @@ -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, ); @@ -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, diff --git a/src/evaluation/eval_context.rs b/src/evaluation/eval_context.rs index 6662c52..327f2d1 100644 --- a/src/evaluation/eval_context.rs +++ b/src/evaluation/eval_context.rs @@ -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)); diff --git a/src/evaluation/mark_duplicate_subform.rs b/src/evaluation/mark_duplicate_subform.rs index 258d979..75c7482 100644 --- a/src/evaluation/mark_duplicate_subform.rs +++ b/src/evaluation/mark_duplicate_subform.rs @@ -48,7 +48,7 @@ pub fn mark_duplicates_canonized_multiple(root_nodes: &Vec) -> 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 @@ -78,7 +78,7 @@ pub fn mark_duplicates_canonized_multiple(root_nodes: &Vec) -> 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 @@ -104,79 +104,6 @@ pub fn mark_duplicates_canonized_single(root_node: &HctlTreeNode) -> HashMap HashMap { - // 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 = 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 = 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[¤t_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 ¤t_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::{ @@ -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(); @@ -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 @@ -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 diff --git a/src/preprocessing/node.rs b/src/preprocessing/node.rs index 2aa2209..bce8ab3 100644 --- a/src/preprocessing/node.rs +++ b/src/preprocessing/node.rs @@ -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, } @@ -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 @@ -62,7 +63,7 @@ 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)), } @@ -70,8 +71,13 @@ impl HctlTreeNode { /// 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)), } @@ -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)), } @@ -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)), } @@ -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)), } @@ -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), } @@ -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) } } @@ -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()); } diff --git a/src/preprocessing/operator_enums.rs b/src/preprocessing/operator_enums.rs index 0e105ac..2d45128 100644 --- a/src/preprocessing/operator_enums.rs +++ b/src/preprocessing/operator_enums.rs @@ -6,12 +6,12 @@ use std::fmt; #[derive(Clone, Debug, Eq, Hash, PartialEq, Ord, PartialOrd)] pub enum UnaryOp { Not, // '~' - Ex, // 'EX' - Ax, // 'AX' - Ef, // 'EF' - Af, // 'AF' - Eg, // 'EG' - Ag, // 'AG' + EX, // 'EX' + AX, // 'AX' + EF, // 'EF' + AF, // 'AF' + EG, // 'EG' + AG, // 'AG' } /// Enum for all possible binary operators occurring in a HCTL formula string. @@ -22,10 +22,10 @@ pub enum BinaryOp { Xor, // '^' Imp, // '=>' Iff, // '<=>' - Eu, // 'EU' - Au, // 'AU' - Ew, // 'EW' - Aw, // 'AW' + EU, // 'EU' + AU, // 'AU' + EW, // 'EW' + AW, // 'AW' } /// Enum for all possible hybrid operators occurring in a HCTL formula string. @@ -53,6 +53,7 @@ impl fmt::Display for UnaryOp { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { match self { UnaryOp::Not => write!(f, "~"), + // temporal operators are displayed as they are c => write!(f, "{c:?}"), } } @@ -66,6 +67,7 @@ impl fmt::Display for BinaryOp { BinaryOp::Xor => write!(f, "^"), BinaryOp::Imp => write!(f, "=>"), BinaryOp::Iff => write!(f, "<=>"), + // temporal operators are displayed as they are c => write!(f, "{c:?}"), } } @@ -73,8 +75,12 @@ impl fmt::Display for BinaryOp { impl fmt::Display for HybridOp { fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - let op = self; - write!(f, "{op:?}") + match self { + HybridOp::Bind => write!(f, "!"), + HybridOp::Exists => write!(f, "3"), + HybridOp::Forall => write!(f, "V"), + HybridOp::Jump => write!(f, "@"), + } } } diff --git a/src/preprocessing/parser.rs b/src/preprocessing/parser.rs index 86cb754..0ac4779 100644 --- a/src/preprocessing/parser.rs +++ b/src/preprocessing/parser.rs @@ -69,10 +69,10 @@ fn is_hybrid(token: &HctlToken) -> bool { fn is_binary_temporal(token: &HctlToken) -> bool { matches!( token, - HctlToken::Binary(BinaryOp::Eu) - | HctlToken::Binary(BinaryOp::Au) - | HctlToken::Binary(BinaryOp::Ew) - | HctlToken::Binary(BinaryOp::Aw) + HctlToken::Binary(BinaryOp::EU) + | HctlToken::Binary(BinaryOp::AU) + | HctlToken::Binary(BinaryOp::EW) + | HctlToken::Binary(BinaryOp::AW) ) } @@ -279,32 +279,27 @@ mod tests { /// Also check that the formula is saved correctly in the tree root. fn test_parse_valid_formulae() { let valid1 = "!{x}: AG EF {x}"; - assert!(parse_hctl_formula(valid1).is_ok()); let tree = parse_hctl_formula(valid1).unwrap(); - assert_eq!(tree.subform_str, "(Bind {x}: (Ag (Ef {x})))".to_string()); + assert_eq!(tree.as_str(), "(!{x}: (AG (EF {x})))"); let valid2 = "!{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y})"; - assert!(parse_hctl_formula(valid2).is_ok()); let tree = parse_hctl_formula(valid2).unwrap(); assert_eq!( - tree.subform_str, - "(Bind {x}: (Exists {y}: ((Jump {x}: ((~ {y}) & (Ax {x}))) & (Jump {y}: (Ax {y})))))" - .to_string() + tree.as_str(), + "(!{x}: (3{y}: ((@{x}: ((~{y}) & (AX {x}))) & (@{y}: (AX {y})))))", ); let valid3 = "3{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y}) & EF ({x} & (!{z}: AX {z})) & EF ({y} & (!{z}: AX {z})) & AX (EF ({x} & (!{z}: AX {z})) ^ EF ({y} & (!{z}: AX {z})))"; - assert!(parse_hctl_formula(valid3).is_ok()); let tree = parse_hctl_formula(valid3).unwrap(); - assert_eq!(tree.subform_str, "(Exists {x}: (Exists {y}: ((Jump {x}: ((~ {y}) & (Ax {x}))) & ((Jump {y}: (Ax {y})) & ((Ef ({x} & (Bind {z}: (Ax {z})))) & ((Ef ({y} & (Bind {z}: (Ax {z})))) & (Ax ((Ef ({x} & (Bind {z}: (Ax {z})))) ^ (Ef ({y} & (Bind {z}: (Ax {z}))))))))))))".to_string()); + assert_eq!(tree.as_str(), "(3{x}: (3{y}: ((@{x}: ((~{y}) & (AX {x}))) & ((@{y}: (AX {y})) & ((EF ({x} & (!{z}: (AX {z})))) & ((EF ({y} & (!{z}: (AX {z})))) & (AX ((EF ({x} & (!{z}: (AX {z})))) ^ (EF ({y} & (!{z}: (AX {z}))))))))))))"); // also test propositions, constants, and other operators (and their parse order) // propositions names should not be modified, constants should be unified to True/False let valid4 = "(prop1 <=> PROP2 | false => 1) AU (True ^ 0)"; - assert!(parse_hctl_formula(valid4).is_ok()); let tree = parse_hctl_formula(valid4).unwrap(); assert_eq!( - tree.subform_str, - "((prop1 <=> ((PROP2 | False) => True)) Au (True ^ False))".to_string() + tree.as_str(), + "((prop1 <=> ((PROP2 | False) => True)) AU (True ^ False))" ); // all formulae must be correctly parsed also using the extended version of HCTL @@ -314,6 +309,40 @@ mod tests { assert!(parse_extended_formula(valid4).is_ok()); } + #[test] + fn test_parse_operator_priority() { + assert_eq!( + "(((((~a) ^ ((~b) & (~c))) | (~d)) => (~e)) <=> (~f))", + parse_hctl_formula("~a ^ ~b & ~c | ~d => ~e <=> ~f") + .unwrap() + .as_str() + ) + } + + #[test] + fn test_parse_operator_associativity() { + assert_eq!( + "(a & (b & c))", + parse_hctl_formula("a & b & c").unwrap().as_str() + ); + assert_eq!( + "(a | (b | c))", + parse_hctl_formula("a | b | c").unwrap().as_str() + ); + assert_eq!( + "(a ^ (b ^ c))", + parse_hctl_formula("a ^ b ^ c").unwrap().as_str() + ); + assert_eq!( + "(a => (b => c))", + parse_hctl_formula("a => b => c").unwrap().as_str() + ); + assert_eq!( + "(a <=> (b <=> c))", + parse_hctl_formula("a <=> b <=> c").unwrap().as_str() + ); + } + #[test] /// Test parsing of several valid HCTL formulae against expected results. fn compare_parser_with_expected() { @@ -327,7 +356,7 @@ mod tests { let formula = "!{x}: (AX {x})"; let expected_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, ); @@ -364,18 +393,15 @@ mod tests { assert!(parse_hctl_formula(formula).is_err()); assert!(parse_extended_formula(formula).is_ok()); let tree = parse_extended_formula(formula).unwrap(); - assert_eq!( - tree.subform_str, - "((Bind {x}: (Ag (Ef {x}))) & %p%)".to_string() - ); + assert_eq!(tree.as_str(), "((!{x}: (AG (EF {x}))) & %p%)"); let formula = "!{x}: 3{y}: (@{x}: ~{y} & %s%) & (@{y}: %s%)"; assert!(parse_hctl_formula(formula).is_err()); assert!(parse_extended_formula(formula).is_ok()); let tree = parse_extended_formula(formula).unwrap(); assert_eq!( - tree.subform_str, - "(Bind {x}: (Exists {y}: ((Jump {x}: ((~ {y}) & %s%)) & (Jump {y}: %s%))))".to_string() + tree.as_str(), + "(!{x}: (3{y}: ((@{x}: ((~{y}) & %s%)) & (@{y}: %s%))))" ); } } diff --git a/src/preprocessing/tokenizer.rs b/src/preprocessing/tokenizer.rs index 487097a..7038cd0 100644 --- a/src/preprocessing/tokenizer.rs +++ b/src/preprocessing/tokenizer.rs @@ -80,11 +80,11 @@ fn try_tokenize_recursive( } match c2 { - 'X' => output.push(HctlToken::Unary(UnaryOp::Ex)), - 'F' => output.push(HctlToken::Unary(UnaryOp::Ef)), - 'G' => output.push(HctlToken::Unary(UnaryOp::Eg)), - 'U' => output.push(HctlToken::Binary(BinaryOp::Eu)), - 'W' => output.push(HctlToken::Binary(BinaryOp::Ew)), + 'X' => output.push(HctlToken::Unary(UnaryOp::EX)), + 'F' => output.push(HctlToken::Unary(UnaryOp::EF)), + 'G' => output.push(HctlToken::Unary(UnaryOp::EG)), + 'U' => output.push(HctlToken::Binary(BinaryOp::EU)), + 'W' => output.push(HctlToken::Binary(BinaryOp::EW)), _ => return Err(format!("Unexpected char '{c2}' after 'E'.")), } } else { @@ -106,11 +106,11 @@ fn try_tokenize_recursive( } } match c2 { - 'X' => output.push(HctlToken::Unary(UnaryOp::Ax)), - 'F' => output.push(HctlToken::Unary(UnaryOp::Af)), - 'G' => output.push(HctlToken::Unary(UnaryOp::Ag)), - 'U' => output.push(HctlToken::Binary(BinaryOp::Au)), - 'W' => output.push(HctlToken::Binary(BinaryOp::Aw)), + 'X' => output.push(HctlToken::Unary(UnaryOp::AX)), + 'F' => output.push(HctlToken::Unary(UnaryOp::AF)), + 'G' => output.push(HctlToken::Unary(UnaryOp::AG)), + 'U' => output.push(HctlToken::Binary(BinaryOp::AU)), + 'W' => output.push(HctlToken::Binary(BinaryOp::AW)), _ => return Err(format!("Unexpected char '{c2}' after 'A'.")), } } else { @@ -313,8 +313,8 @@ mod tests { tokens1, vec![ HctlToken::Hybrid(HybridOp::Bind, "x".to_string()), - HctlToken::Unary(UnaryOp::Ag), - HctlToken::Unary(UnaryOp::Ef), + HctlToken::Unary(UnaryOp::AG), + HctlToken::Unary(UnaryOp::EF), HctlToken::Atom(Atomic::Var("x".to_string())), ] ); @@ -327,12 +327,12 @@ mod tests { vec![ HctlToken::Hybrid(HybridOp::Bind, "x".to_string()), HctlToken::Tokens(vec![ - HctlToken::Unary(UnaryOp::Ax), + HctlToken::Unary(UnaryOp::AX), HctlToken::Tokens(vec![ HctlToken::Unary(UnaryOp::Not), HctlToken::Atom(Atomic::Var("x".to_string())), HctlToken::Binary(BinaryOp::And), - HctlToken::Unary(UnaryOp::Af), + HctlToken::Unary(UnaryOp::AF), HctlToken::Atom(Atomic::Var("x".to_string())), ]), ]), @@ -352,13 +352,13 @@ mod tests { HctlToken::Unary(UnaryOp::Not), HctlToken::Atom(Atomic::Var("y".to_string())), HctlToken::Binary(BinaryOp::And), - HctlToken::Unary(UnaryOp::Ax), + HctlToken::Unary(UnaryOp::AX), HctlToken::Atom(Atomic::Var("x".to_string())), ]), HctlToken::Binary(BinaryOp::And), HctlToken::Tokens(vec![ HctlToken::Hybrid(HybridOp::Jump, "y".to_string()), - HctlToken::Unary(UnaryOp::Ax), + HctlToken::Unary(UnaryOp::AX), HctlToken::Atom(Atomic::Var("y".to_string())), ]), ] @@ -380,10 +380,10 @@ mod tests { HctlToken::Binary(BinaryOp::Imp), HctlToken::Atom(Atomic::Prop("1".to_string())), ]), - HctlToken::Binary(BinaryOp::Eu), + HctlToken::Binary(BinaryOp::EU), HctlToken::Tokens(vec![ HctlToken::Atom(Atomic::Prop("0".to_string())), - HctlToken::Binary(BinaryOp::Aw), + HctlToken::Binary(BinaryOp::AW), HctlToken::Atom(Atomic::Prop("A_prop".to_string())), HctlToken::Binary(BinaryOp::Xor), HctlToken::Atom(Atomic::Prop("E_prop".to_string())),