automation-structures 0.2.2

Reusable, formally specified building blocks for composing automation systems.
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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68

//! Reusable boolean marker relations.

use vstd::prelude::*;

verus! {

/// Set a marker when selected and otherwise preserve it.
pub open spec fn set_if(before: bool, after: bool, selected: bool) -> bool {
    after == if selected { true } else { before }
}

/// A selected transition that leaves the marker clear is rejected.
pub proof fn selected_unset_rejected(before: bool)
    ensures !set_if(before, false, true),
{
}

/// Clear a marker when selected and otherwise preserve it.
pub open spec fn clear_if(before: bool, after: bool, selected: bool) -> bool {
    after == if selected { false } else { before }
}

/// A reusable retained boolean marker.
#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
pub struct Marker {
    /// Retained marker state.
    pub marked: bool,
}

impl Marker {
    /// Construct a marker with an explicit initial state.
    pub fn new(marked: bool) -> (marker: Self)
        ensures marker.marked == marked,
    {
        Self { marked }
    }

    /// Whether the marker is set.
    pub fn is_marked(&self) -> (marked: bool)
        ensures marked == self.marked,
    {
        self.marked
    }

    /// Set the marker and return whether its state changed.
    pub fn set(&mut self) -> (changed: bool)
        ensures
            final(self).marked,
            changed == !old(self).marked,
    {
        let changed = !self.marked;
        self.marked = true;
        changed
    }

    /// Clear the marker and return whether its state changed.
    pub fn clear(&mut self) -> (changed: bool)
        ensures
            !final(self).marked,
            changed == old(self).marked,
    {
        let changed = self.marked;
        self.marked = false;
        changed
    }
}

}