automation-structures 0.1.1

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

//! 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 }
}

}