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

use machine_check_common::iir::property::IProperty;
use serde::{Deserialize, Serialize};
use snapshot::Snapshot;

use crate::shared::snapshot::PropertyIndex;

pub mod snapshot;

/// Step settings.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct StepSettings {
    pub max_refinements: Option<u64>,
    pub selected_property: IProperty,
}

/// Request for the backend to do something.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub enum Request {
    InitialContent,
    GetContent,
    Query,
    Cancel,
    Reset,
    Step(StepSettings),
    AddProperty(String),
    RemoveProperty(PropertyIndex),
}

/// Backend status.
#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq)]
pub enum BackendStatus {
    Cancelling,
    Waiting,
    Running,
}

impl BackendStatus {
    pub fn is_waiting(&self) -> bool {
        matches!(self, BackendStatus::Waiting)
    }
}

#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq)]
pub struct BackendSpaceInfo {
    pub num_refinements: usize,
    pub num_states: usize,
    pub num_transitions: usize,
}

/// Information about the backend.
#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq)]
pub struct BackendInfo {
    pub status: BackendStatus,
    pub space_info: BackendSpaceInfo,
}

/// Response from the backend to a request from the frontend.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct Response {
    pub info: BackendInfo,
    pub snapshot: Option<Snapshot>,
}