Lines
51.63 %
Functions
61.54 %
Branches
100 %
use std::ops::ControlFlow;
use merc_utilities::MercError;
use crate::{RegFrm, StateFrm};
/// Applies the given function recursively to the state formula.
///
/// The substitution function takes a state formula and returns an optional new
/// formula. If it returns `Some(new_formula)`, the substitution is applied and
/// the new formula is returned. If it returns `None`, the substitution is not
/// applied and the function continues to traverse the formula tree.
pub fn apply_statefrm<F>(
formula: StateFrm,
mut function: F,
) -> Result<StateFrm, MercError>
where F: FnMut(&StateFrm) -> Result<Option<StateFrm>, MercError>
{
apply_statefrm_rec(formula, &mut function)
}
/// Visits the state formula and calls the given function on each subformula.
/// The visitor function takes a state formula and returns a `ControlFlow`. If
/// it returns `ControlFlow::Break(value)`, the traversal is stopped and the
/// value is returned. If it returns `ControlFlow::Continue(())`, the traversal
/// continues.
pub fn visit_statefrm<T>(
formula: &StateFrm,
mut visitor: impl FnMut(&StateFrm) -> Result<ControlFlow<T>, MercError>,
) -> Result<Option<T>, MercError> {
visit_statefrm_rec(formula, &mut visitor)
/// See [`apply`].
fn apply_statefrm_rec<F>(
apply: &mut F,
if let Some(formula) = apply(&formula)? {
// A substitution was made, return the new formula.
return Ok(formula);
match formula {
StateFrm::Binary { op, lhs, rhs } => {
let new_lhs = apply_statefrm_rec(*lhs, apply)?;
let new_rhs = apply_statefrm_rec(*rhs, apply)?;
Ok(StateFrm::Binary {
op,
lhs: Box::new(new_lhs),
rhs: Box::new(new_rhs),
})
StateFrm::FixedPoint {
operator,
variable,
body,
} => {
let new_body = apply_statefrm_rec(*body, apply)?;
Ok(StateFrm::FixedPoint {
body: Box::new(new_body),
StateFrm::Bound { bound, variables, body } => {
Ok(StateFrm::Bound {
bound,
variables,
StateFrm::Modality {
formula,
expr,
let expr = apply_statefrm_rec(*expr, apply)?;
Ok(StateFrm::Modality {
expr: Box::new(expr),
StateFrm::Quantifier {
quantifier,
Ok(StateFrm::Quantifier {
StateFrm::DataValExprRightMult(expr, data_val) => {
let new_expr = apply_statefrm_rec(*expr, apply)?;
Ok(StateFrm::DataValExprRightMult(Box::new(new_expr), data_val))
StateFrm::DataValExprLeftMult(data_val, expr) => {
Ok(StateFrm::DataValExprLeftMult(data_val, Box::new(new_expr)))
StateFrm::Unary { op, expr } => {
Ok(StateFrm::Unary {
expr: Box::new(new_expr),
StateFrm::Id(_, _)
| StateFrm::True
| StateFrm::False
| StateFrm::Delay(_)
| StateFrm::Yaled(_)
| StateFrm::DataValExpr(_) => Ok(formula),
/// See [`visit`].
fn visit_statefrm_rec<T>(
function: &mut impl FnMut(&StateFrm) -> Result<ControlFlow<T>, MercError>,
if let ControlFlow::Break(result) = function(formula)? {
// The visitor requested to break the traversal.
return Ok(Some(result));
StateFrm::Binary { lhs, rhs, .. } => {
visit_statefrm_rec(lhs, function)?;
visit_statefrm_rec(rhs, function)?;
StateFrm::FixedPoint { body, .. } => {
visit_statefrm_rec(body, function)?;
StateFrm::Bound { body, .. } => {
StateFrm::Modality { expr, .. } => {
visit_statefrm_rec(expr, function)?;
StateFrm::Quantifier { body, .. } => {
StateFrm::DataValExprRightMult(expr, _data_val) => {
StateFrm::DataValExprLeftMult(_data_val, expr) => {
StateFrm::Unary { expr, .. } => {
| StateFrm::DataValExpr(_) => {}
// The visitor did not break the traversal.
Ok(None)
/// Applies the given function recursively to the regular formula. The
/// substitution function takes a regular formula and returns an optional new
pub fn apply_regular_formula<F>(
formula: RegFrm,
) -> Result<RegFrm, MercError>
where F: FnMut(&RegFrm) -> Result<Option<RegFrm>, MercError>
apply_regular_formula_rec(formula, &mut function)
/// See [apply_regular_formula].
fn apply_regular_formula_rec<F>(formula: RegFrm, apply: &mut F) -> Result<RegFrm, MercError>
RegFrm::Iteration(reg_frm) => {
let new_reg_frm = apply_regular_formula_rec(*reg_frm, apply)?;
Ok(RegFrm::Iteration(Box::new(new_reg_frm)))
RegFrm::Plus(reg_frm) => {
Ok(RegFrm::Plus(Box::new(new_reg_frm)))
RegFrm::Sequence { lhs, rhs } => {
let new_lhs = apply_regular_formula_rec(*lhs, apply)?;
let new_rhs = apply_regular_formula_rec(*rhs, apply)?;
Ok(RegFrm::Sequence {
RegFrm::Choice { lhs, rhs } => {
Ok(RegFrm::Choice {
_ => Ok(formula),
#[cfg(test)]
mod tests {
use std::vec;
use crate::UntypedStateFrmSpec;
use super::*;
#[test]
fn test_visit_state_frm_variables() {
let input = UntypedStateFrmSpec::parse("mu X. [a]X && mu X. X && Y").unwrap();
let mut variables = vec![];
apply_statefrm(input.formula, |frm| {
if let StateFrm::Id(name, _) = frm {
variables.push(name.clone());
.unwrap();
assert_eq!(variables, vec!["X", "X", "Y"]);