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

use super::{util::web_idl::get_element_by_id, view::View};
use crate::shared::{BackendInfo, BackendStatus, Request};

mod canvas;
mod control;
mod input;
mod text;
mod tick;

/// Initialises the frontend DOM page.
pub async fn init() {
    // get the initial content first to provide the initial view
    let response = control::call_backend(Request::InitialContent).await;
    let Some(snapshot) = response.snapshot else {
        panic!("Initial content should have a snapshot");
    };
    let initial_view = View::new(snapshot, response.info);
    view_singleton::provide_initial_view(initial_view);

    canvas::init();
    input::init();
    control::init();
    tick::init();

    // make sure rendering occurs
    let mut view_guard = lock_view();
    render(view_guard.as_mut());
}

/// Issues a command to the backend and processes the result.
async fn issue_command(request: Request) {
    let is_query = matches!(request, Request::Query);
    let mut response = control::call_backend(request).await;
    if is_query {
        {
            let mut view_guard = lock_view();
            let view = view_guard.as_mut();

            if *view.backend_info() == response.info {
                // no change, do nothing
                return;
            }

            if view.backend_info().status.is_waiting() || !response.info.status.is_waiting() {
                // the query should not result in content get
                // just update and display the info
                view.update_backend_info(response.info);
                display_backend_info(view.backend_info());
                return;
            }
            view.update_backend_info(response.info);
        }
        response = control::call_backend(Request::GetContent).await;
    }

    // update the view with the snapshot and backend status and render
    let mut view_guard = lock_view();
    let view = view_guard.as_mut();
    view.update_backend_info(response.info);
    if let Some(snapshot) = response.snapshot {
        view.apply_snapshot(snapshot);
        render(view);
    } else {
        display_backend_info(view.backend_info());
    }
}

/// Renders the frontend view into the DOM page.
fn render(view: &mut View) {
    display_backend_info(view.backend_info());
    canvas::render(view);
    text::display(view);
}

/// Displays received backend info in the DOM page.
fn display_backend_info(backend_info: &BackendInfo) {
    let backend_status = &backend_info.status;
    let (status_class, status_str) = match backend_status {
        BackendStatus::Waiting => ("waiting", "Waiting"),
        BackendStatus::Running => ("running", "Running"),
        BackendStatus::Cancelling => ("cancelling", "Cancelling"),
    };
    let info_middle_element = get_element_by_id("info");
    info_middle_element
        .class_list()
        .remove_3("waiting", "running", "cancelling")
        .unwrap();
    info_middle_element
        .class_list()
        .add_1(status_class)
        .unwrap();

    let status_element = get_element_by_id("verification_status");
    status_element.set_text_content(Some(status_str));
    control::display_backend_status(backend_status);

    let space_info_element = get_element_by_id("space_info");

    let info = &backend_info.space_info;
    space_info_element.set_text_content(Some(&format!(
        "{} refinements, {} states, {} transitions",
        info.num_refinements, info.num_states, info.num_transitions
    )));
}

/// The view singleton.
///
/// In its own scope so it cannot be manipulated easily.
mod view_singleton {
    use std::sync::{LazyLock, Mutex, MutexGuard};

    use crate::frontend::view::View;

    static VIEW: LazyLock<Mutex<Option<View>>> = LazyLock::new(|| Mutex::new(None));

    pub struct ViewGuard {
        guard: MutexGuard<'static, Option<View>>,
    }

    impl ViewGuard {
        pub fn as_ref(&self) -> &View {
            self.guard
                .as_ref()
                .expect("View should be initially provided")
        }

        pub fn as_mut(&mut self) -> &mut View {
            self.guard
                .as_mut()
                .expect("View should be initially provided")
        }
    }

    pub fn lock_view() -> ViewGuard {
        ViewGuard {
            guard: VIEW.lock().expect("View should not be poisoned"),
        }
    }

    pub(super) fn provide_initial_view(view: View) {
        VIEW.lock()
            .expect("View should not be poisoned")
            .replace(view);
    }
}

use view_singleton::lock_view;