machine-check-gui 0.7.1

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
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159

use wasm_bindgen::JsCast;
use web_sys::{HtmlButtonElement, HtmlInputElement};

use crate::frontend::util::web_idl::document;
use crate::shared::{Request, StepSettings};
use crate::{
    frontend::{
        client::{issue_command, view_singleton::lock_view},
        util::web_idl::{get_element_by_id, setup_selector_listener},
    },
    shared::BackendStatus,
};

pub fn init() {
    setup_selector_listener(
        "#reset",
        "click",
        Box::new(|_e| {
            wasm_bindgen_futures::spawn_local(on_reset_click());
        }),
    );

    setup_selector_listener(
        "#step",
        "click",
        Box::new(|_e| {
            wasm_bindgen_futures::spawn_local(on_step_click());
        }),
    );

    setup_selector_listener(
        "#run",
        "click",
        Box::new(|_e| {
            wasm_bindgen_futures::spawn_local(on_run_click());
        }),
    );
}

pub fn display_backend_status(backend_status: &BackendStatus) {
    let reset_element: HtmlButtonElement = get_element_by_id("reset").dyn_into().unwrap();
    let step_element: HtmlButtonElement = get_element_by_id("step").dyn_into().unwrap();
    let run_element: HtmlButtonElement = get_element_by_id("run").dyn_into().unwrap();

    let mut step_active = false;
    let mut run_active = false;
    let document = document();
    if let Some(active_element) = document.active_element() {
        if active_element == **step_element {
            step_active = true;
        } else if active_element == **run_element {
            run_active = true;
        }
    }

    const DATA_ACTIVE: &str = "data-active";

    match backend_status {
        BackendStatus::Cancelling => {
            reset_element.set_disabled(true);
            step_element.set_disabled(true);
            run_element.set_disabled(true);

            if run_active && run_element.get_attribute(DATA_ACTIVE).is_none() {
                run_element.set_attribute(DATA_ACTIVE, "run").unwrap();
            }
        }
        BackendStatus::Waiting => {
            reset_element.set_disabled(false);
            step_element.set_disabled(false);
            run_element.set_disabled(false);

            match run_element.get_attribute(DATA_ACTIVE).as_deref() {
                Some("step") => {
                    step_element.focus().unwrap();
                }
                Some("run") => {
                    run_element.focus().unwrap();
                }
                _ => {}
            };
            run_element.remove_attribute(DATA_ACTIVE).unwrap();
        }
        BackendStatus::Running => {
            reset_element.set_disabled(true);
            step_element.set_disabled(true);
            run_element.set_disabled(false);

            if step_active {
                run_element.set_attribute(DATA_ACTIVE, "step").unwrap();
                // refocus on the run element, which now acts as cancellation
                run_element.focus().unwrap();
            }
        }
    }

    if backend_status.is_waiting() {
        // play symbol
        run_element.set_inner_text("\u{23F5}");
    } else {
        // pause symbol
        run_element.set_inner_text("\u{23F8}");
    }
}

pub async fn on_reset_click() {
    issue_command(Request::Reset).await;
}

pub async fn on_step_click() {
    let input: HtmlInputElement = get_element_by_id("max_refinements")
        .dyn_into()
        .expect("The number of steps element should be an input");

    let max_refinements = (input.value_as_number() as u64).max(1);

    issue_step(Some(max_refinements)).await;
}

pub async fn on_run_click() {
    // depending on whether we are waiting, either run or cancel
    let waiting = {
        let view_guard = lock_view();
        view_guard.as_ref().backend_info().status.is_waiting()
    };

    if waiting {
        issue_step(None).await;
    } else {
        issue_command(Request::Cancel).await;
    }
}

pub async fn issue_step(max_refinements: Option<u64>) {
    let selected_property = {
        let view_guard = lock_view();

        // select the property to use for stepping
        // use the root property, not the subproperty, as we are interested
        // in whether the root property holds or not
        let Some(selected_property) = view_guard.as_ref().selected_property_index() else {
            // if no property is selected, just quietly return
            return;
        };

        view_guard
            .as_ref()
            .snapshot()
            .property_snapshot(selected_property)
            .property
            .clone()
    };

    issue_command(Request::Step(StepSettings {
        max_refinements,
        selected_property,
    }))
    .await;
}