vstd_extra/state_machine/
action.rs

1// Copyright 2022 VMware, Inc.
2// SPDX-License-Identifier: MIT
3#![allow(unused_imports)]
4use super::super::temporal_logic::*;
5use vstd::prelude::*;
6
7verus! {
8
9#[verifier(reject_recursive_types(State))]
10#[verifier(reject_recursive_types(Input))]
11#[verifier(reject_recursive_types(Output))]
12pub struct Action<State, Input, Output> {
13    // The condition that enables the host action.
14    pub precondition: spec_fn(Input, State) -> bool,
15    // The new internal state and output made by the transition.
16    pub transition: spec_fn(Input, State) -> (State, Output),
17}
18
19impl<State, Input, Output> Action<State, Input, Output> {
20    pub open spec fn pre(self, input: Input) -> StatePred<State> {
21        StatePred::new(|s: State| (self.precondition)(input, s))
22    }
23
24    pub open spec fn forward(self, input: Input) -> ActionPred<State> {
25        ActionPred::new(
26            |s: State, s_prime: State|
27                {
28                    &&& (self.precondition)(input, s)
29                    &&& s_prime == (self.transition)(input, s).0
30                },
31        )
32    }
33
34    // `weak_fairness` assumption says that,
35    // it is always true that, if `pre` is always true, `forward` eventually becomes true
36    pub open spec fn weak_fairness(self, input: Input) -> TempPred<State> {
37        always(lift_state(self.pre(input))).leads_to(lift_action(self.forward(input)))
38    }
39
40    // `wf1` is a specialized version of temporal_logic_rules::wf1 for Action
41    pub proof fn wf1(
42        self,
43        input: Input,
44        spec: TempPred<State>,
45        next: ActionPred<State>,
46        pre: StatePred<State>,
47        post: StatePred<State>,
48    )
49        requires
50            forall|s, s_prime: State|
51                pre.apply(s) && #[trigger] next.apply(s, s_prime) ==> pre.apply(s_prime)
52                    || post.apply(s_prime),
53            forall|s, s_prime: State|
54                pre.apply(s) && #[trigger] next.apply(s, s_prime) && self.forward(input).apply(
55                    s,
56                    s_prime,
57                ) ==> post.apply(s_prime),
58            spec.entails(always(lift_action(next))),
59            spec.entails(always(lift_state(pre).implies(lift_state(self.pre(input))))),
60            spec.entails(self.weak_fairness(input)),
61        ensures
62            spec.entails(lift_state(pre).leads_to(lift_state(post))),
63    {
64        always_implies_preserved_by_always::<State>(
65            spec,
66            lift_state(pre),
67            lift_state(self.pre(input)),
68        );
69        leads_to_weaken::<State>(
70            spec,
71            always(lift_state(self.pre(input))),
72            lift_action(self.forward(input)),
73            always(lift_state(pre)),
74            lift_action(self.forward(input)),
75        );
76        wf1_variant_temp::<State>(
77            spec,
78            lift_action(next),
79            lift_action(self.forward(input)),
80            lift_state(pre),
81            lift_state(post),
82        );
83    }
84
85    pub proof fn lemma_statisfy_pre_implies_enabled(self, input: Input, state: State)
86        requires
87            self.pre(input).apply(state),
88        ensures
89            enabled(self.forward(input)).apply(state),
90    {
91        let (new_state, _output) = (self.transition)(input, state);
92        assert(self.forward(input).apply(state, new_state));
93    }
94}
95
96pub enum ActionResult<State, Output> {
97    Disabled,
98    Enabled(State, Output),
99}
100
101} // verus!
vstd_extra/state_machine/action.rs

vstd_extra/state_machine/
action.rs
