use quint_connect::*;
use serde::Deserialize;
#[derive(Debug, Eq, PartialEq, Deserialize)]
struct TuiState {
phase: String,
dirty: bool,
#[serde(rename = "reportDirty")]
report_dirty: bool,
#[serde(rename = "reportComputing")]
report_computing: bool,
#[serde(rename = "reportReady")]
report_ready: bool,
#[serde(rename = "walEvents")]
wal_events: i64,
#[serde(rename = "manualRefreshes")]
manual_refreshes: i64,
refreshes: i64,
#[serde(rename = "reportPublishes")]
report_publishes: i64,
#[serde(rename = "totalSessions")]
total_sessions: i64,
cursor: i64,
#[serde(rename = "fetchedStart")]
fetched_start: i64,
#[serde(rename = "fetchedEnd")]
fetched_end: i64,
#[serde(rename = "pageLoading")]
page_loading: bool,
#[serde(rename = "loadRequests")]
load_requests: i64,
}
#[derive(Debug)]
struct TuiDriver {
phase: String,
dirty: bool,
report_dirty: bool,
report_computing: bool,
report_ready: bool,
wal_events: i64,
manual_refreshes: i64,
refreshes: i64,
report_publishes: i64,
total_sessions: i64,
cursor: i64,
fetched_start: i64,
fetched_end: i64,
page_loading: bool,
load_requests: i64,
}
impl Default for TuiDriver {
fn default() -> Self {
Self {
phase: "Boot".into(),
dirty: false,
report_dirty: true,
report_computing: false,
report_ready: false,
wal_events: 0,
manual_refreshes: 0,
refreshes: 0,
report_publishes: 0,
total_sessions: 0,
cursor: 0,
fetched_start: 0,
fetched_end: 0,
page_loading: false,
load_requests: 0,
}
}
}
impl State<TuiDriver> for TuiState {
fn from_driver(d: &TuiDriver) -> Result<Self> {
Ok(TuiState {
phase: d.phase.clone(),
dirty: d.dirty,
report_dirty: d.report_dirty,
report_computing: d.report_computing,
report_ready: d.report_ready,
wal_events: d.wal_events,
manual_refreshes: d.manual_refreshes,
refreshes: d.refreshes,
report_publishes: d.report_publishes,
total_sessions: d.total_sessions,
cursor: d.cursor,
fetched_start: d.fetched_start,
fetched_end: d.fetched_end,
page_loading: d.page_loading,
load_requests: d.load_requests,
})
}
}
impl Driver for TuiDriver {
type State = TuiState;
fn step(&mut self, step: &Step) -> Result {
switch!(step {
init => {
*self = Self::default();
},
step => {
*self = Self::default();
},
become_ready => {
require_phase(&self.phase, "Boot", "become_ready")?;
self.phase = "Interactive".into();
},
wal_change => {
require_phase(&self.phase, "Interactive", "wal_change")?;
self.dirty = true;
self.wal_events += 1;
},
coalesced_refresh => {
require_phase(&self.phase, "Interactive", "coalesced_refresh")?;
if !self.dirty {
anyhow::bail!("coalesced_refresh not enabled");
}
self.dirty = false;
self.report_dirty = true;
self.refreshes += 1;
},
manual_refresh => {
require_phase(&self.phase, "Interactive", "manual_refresh")?;
self.dirty = false;
self.report_dirty = true;
self.manual_refreshes += 1;
self.refreshes += 1;
},
report_recompute => {
require_phase(&self.phase, "Interactive", "report_recompute")?;
if !self.report_dirty || self.report_computing {
anyhow::bail!("report_recompute not enabled");
}
self.report_dirty = false;
self.report_computing = true;
},
report_publish => {
require_phase(&self.phase, "Interactive", "report_publish")?;
if !self.report_computing {
anyhow::bail!("report_publish not enabled");
}
self.report_computing = false;
self.report_ready = true;
self.report_publishes += 1;
},
page_load_request => {
require_phase(&self.phase, "Interactive", "page_load_request")?;
if self.page_loading {
anyhow::bail!("page_load_request double-load");
}
self.page_loading = true;
self.load_requests += 1;
},
page_load_complete => {
require_phase(&self.phase, "Interactive", "page_load_complete")?;
if !self.page_loading {
anyhow::bail!("page_load_complete not enabled");
}
self.total_sessions = 20;
self.fetched_start = 0;
self.fetched_end = 20;
self.page_loading = false;
},
scroll_down => {
require_phase(&self.phase, "Interactive", "scroll_down")?;
if self.total_sessions <= 0
|| self.cursor + 1 >= self.total_sessions
|| self.cursor + 1 >= self.fetched_end
{
anyhow::bail!("scroll_down not enabled");
}
self.cursor += 1;
},
filter_reset => {
require_phase(&self.phase, "Interactive", "filter_reset")?;
self.total_sessions = 0;
self.cursor = 0;
self.fetched_start = 0;
self.fetched_end = 0;
self.page_loading = false;
},
request_quit => {
require_phase(&self.phase, "Interactive", "request_quit")?;
self.phase = "Draining".into();
},
finish_shutdown => {
require_phase(&self.phase, "Draining", "finish_shutdown")?;
self.phase = "Exited".into();
},
})
}
}
fn require_phase(actual: &str, expected: &str, action: &str) -> Result<()> {
if actual != expected {
anyhow::bail!("{action} not enabled");
}
Ok(())
}
#[quint_run(
spec = "specs/tui-app.qnt",
max_samples = 20,
max_steps = 10,
seed = "0x7"
)]
fn tui_app_run() -> impl Driver {
TuiDriver::default()
}