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

use std::time::Duration;

use chrono::{DateTime, Local, Timelike};
use wasm_bindgen::JsCast;
use web_sys::{Element, HtmlTableRowElement};

use crate::{
    frontend::{
        util::web_idl::{document, get_element_by_id},
        view::View,
    },
    shared::snapshot::log::MessageType,
};

pub fn display(view: &View) {
    LogDisplayer::new(view).display();
}

struct LogDisplayer<'a> {
    view: &'a View,
    log_wrapper_element: Element,
    log_body_element: Element,
}

impl LogDisplayer<'_> {
    fn new(view: &View) -> LogDisplayer {
        let log_wrapper_element = get_element_by_id("log_wrapper");
        let log_body_element = get_element_by_id("log").first_element_child().unwrap();
        let log_body_element = log_body_element.dyn_into().unwrap();
        LogDisplayer {
            view,
            log_wrapper_element,
            log_body_element,
        }
    }

    fn display(&self) {
        let previous_num_children = self.log_body_element.child_element_count();

        // remove all children except the first (table header)
        let first_child = self.log_body_element.first_element_child().unwrap();
        self.log_body_element.set_inner_html("");
        self.log_body_element.append_child(&first_child).unwrap();

        for message in &self.view.snapshot().log.messages {
            let row_element: HtmlTableRowElement =
                document().create_element("tr").unwrap().dyn_into().unwrap();

            let time_element = row_element.insert_cell().unwrap();
            let duration_element = row_element.insert_cell().unwrap();
            duration_element.set_text_content(Some("-"));
            let type_element = row_element.insert_cell().unwrap();
            let message_element = row_element.insert_cell().unwrap();

            let local_time: DateTime<Local> = message.time.into();

            time_element.set_text_content(Some(&pretty_time(&local_time)));

            match &message.ty {
                MessageType::Error(msg) => {
                    type_element.set_text_content(Some("Error"));
                    message_element.set_text_content(Some(&format!("Error: {}", msg)));
                }
                MessageType::Step(step_message) => {
                    duration_element
                        .set_text_content(Some(&pretty_duration(&step_message.duration)));
                    type_element.set_text_content(Some("Step"));
                    message_element.set_text_content(Some(&format!(
                        "{} after {} refinements.",
                        match step_message.status {
                            crate::shared::snapshot::log::StepStatus::Completed => "Completed",
                            crate::shared::snapshot::log::StepStatus::Cancelled => "Cancelled",
                        },
                        step_message.num_refinements
                    )));
                }
                MessageType::Reset => {
                    type_element.set_text_content(Some("Reset"));
                    message_element
                        .set_text_content(Some("The verification framework has been reset."));
                }
            }

            self.log_body_element.append_child(&row_element).unwrap();
        }

        let num_children = self.log_body_element.child_element_count();

        if num_children > previous_num_children {
            // new messages, scroll down
            self.log_wrapper_element
                .set_scroll_top(self.log_wrapper_element.scroll_height());
        }
    }
}

fn pretty_time(time: &DateTime<Local>) -> String {
    // just write the time in hours, minutes, and seconds
    // it just serves as a way to recall things
    let time = time.time();
    format!(
        "{:0>2}:{:0>2}:{:0>2}",
        time.hour(),
        time.minute(),
        time.second()
    )
}

fn pretty_duration(duration: &Duration) -> String {
    const SECONDS_IN_MINUTE: u64 = 60;
    const SECONDS_IN_HOUR: u64 = SECONDS_IN_MINUTE * 60;
    let seconds = duration.as_secs();
    let hours = seconds / SECONDS_IN_HOUR;
    let seconds = seconds % SECONDS_IN_HOUR;
    let minutes = seconds / SECONDS_IN_MINUTE;
    let seconds = seconds % SECONDS_IN_MINUTE;

    let millis = duration.subsec_millis();

    if hours == 0 {
        if minutes == 0 {
            format!("{}.{:0>3} s", seconds, millis)
        } else {
            format!("{}:{:0>2}.{:0>3} s", minutes, seconds, millis)
        }
    } else {
        format!("{}:{:0>2}:{:0>2}.{:0>3} s", hours, minutes, seconds, millis)
    }
}