machine-check-common 0.4.0

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31

use super::{Property, TemporalOperator};

impl Property {
    pub(crate) fn contains_negation(&self) -> bool {
        match self {
            Property::Const(_) => false,
            Property::Atomic(_) => false,
            Property::Negation(_) => true,
            Property::Or(bi) => bi.a.contains_negation() || bi.b.contains_negation(),
            Property::And(bi) => bi.a.contains_negation() || bi.b.contains_negation(),
            Property::E(temporal) => temporal.contains_negation(),
            Property::A(temporal) => temporal.contains_negation(),
        }
    }
}

impl TemporalOperator {
    fn contains_negation(&self) -> bool {
        match self {
            TemporalOperator::X(inner) => inner.0.contains_negation(),
            TemporalOperator::F(inner) => inner.0.contains_negation(),
            TemporalOperator::G(inner) => inner.0.contains_negation(),
            TemporalOperator::U(inner) => {
                inner.hold.contains_negation() || inner.until.contains_negation()
            }
            TemporalOperator::R(inner) => {
                inner.releaser.contains_negation() || inner.releasee.contains_negation()
            }
        }
    }
}