tessellate-core 0.5.0

//! Deterministic bounded exploration for finite Tess state machines.

use crate::analysis::{AnalysisOptions, AnalysisVerdict};
use crate::ast::{FieldDecl, NumericLiteral, TraceDecl, TransitionDecl, TypeRef};
use crate::compiler::{CompiledProgram, normalize_name};
use crate::engine::{
    Input, ValueEvaluation, evaluate_condition, evaluate_value, validate_field_value,
};
use crate::value::{TruthValue, Value};
use serde::{Deserialize, Serialize};
use std::collections::{BTreeMap, BTreeSet};
use std::fmt::Write;

const STATE_BINDING: &str = "__tess_state";

/// Whether every state and transition inside the requested bound was explored.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum TraceCompleteness {
    BoundedExhaustive,
    Truncated,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum TraceCounterexampleKind {
    NoInitialState,
    InitialConflict,
    InvariantViolation,
    EvaluationConflict,
    InvalidUpdate,
    DeadEnd,
    NonTermination,
}

/// One state in a replayable counterexample path.
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
pub struct TraceState {
    pub fields: BTreeMap<String, Value>,
}

/// The transition is absent for the initial state and present on every later step.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct TraceStep {
    pub depth: usize,
    #[serde(skip_serializing_if = "Option::is_none")]
    pub transition: Option<String>,
    #[serde(skip_serializing_if = "Option::is_none")]
    pub action: Option<String>,
    pub state: TraceState,
}

/// A transition that failed before it could produce the next path state.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct TraceAttempt {
    pub transition: String,
    pub action: String,
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct TraceCounterexample {
    pub kind: TraceCounterexampleKind,
    pub reason: String,
    pub path: Vec<TraceStep>,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub attempted: Option<TraceAttempt>,
}

#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct TraceAnalysis {
    pub trace: String,
    pub verdict: AnalysisVerdict,
    pub bound: usize,
    pub evaluated_states: usize,
    pub reachable_states: usize,
    pub completeness: TraceCompleteness,
    pub counterexamples: Vec<TraceCounterexample>,
    #[serde(default, skip_serializing_if = "Vec::is_empty")]
    pub notes: Vec<String>,
}

impl TraceAnalysis {
    #[must_use]
    pub fn render_text(&self) -> String {
        let mut output = String::new();
        let (marker, verdict) = match self.verdict {
            AnalysisVerdict::Passed => ("✓", "bounded trace proved"),
            AnalysisVerdict::Failed => ("✗", "trace counterexample found"),
            AnalysisVerdict::Inconclusive => ("?", "trace analysis inconclusive"),
        };
        let _ = writeln!(output, "{marker} {}", self.trace);
        let _ = writeln!(
            output,
            "  {verdict} · {} reachable states · within {} steps",
            self.reachable_states, self.bound
        );
        for note in &self.notes {
            let _ = writeln!(output, "  reason · {note}");
        }
        for counterexample in &self.counterexamples {
            let kind = match counterexample.kind {
                TraceCounterexampleKind::NoInitialState => "no initial state",
                TraceCounterexampleKind::InitialConflict => "initial conflict",
                TraceCounterexampleKind::InvariantViolation => "assertion violation",
                TraceCounterexampleKind::EvaluationConflict => "evaluation conflict",
                TraceCounterexampleKind::InvalidUpdate => "invalid update",
                TraceCounterexampleKind::DeadEnd => "dead end",
                TraceCounterexampleKind::NonTermination => "non-termination",
            };
            let _ = writeln!(output, "\n  counterexample · {kind}");
            let _ = writeln!(output, "    reason · {}", counterexample.reason);
            for step in &counterexample.path {
                let via = step.transition.as_ref().map_or_else(
                    || "initial".to_owned(),
                    |transition| {
                        let action = step.action.as_deref().unwrap_or("<unknown action>");
                        format!("{action} / {transition}")
                    },
                );
                let _ = writeln!(output, "    [{}] {via}", step.depth);
                for (field, value) in &step.state.fields {
                    let _ = writeln!(output, "      {field}: {value}");
                }
            }
            if let Some(attempted) = &counterexample.attempted {
                let _ = writeln!(
                    output,
                    "    attempted · {} / {}",
                    attempted.action, attempted.transition
                );
            }
        }
        output
    }
}

#[derive(Clone, Debug)]
struct FrontierNode {
    state: TraceState,
    path: Vec<TraceStep>,
}

/// Analyze all (or one selected) bounded trace declarations.
#[must_use]
pub fn analyze_traces(
    program: &CompiledProgram,
    selected_trace: Option<&str>,
    options: &AnalysisOptions,
) -> Vec<TraceAnalysis> {
    program
        .traces()
        .values()
        .filter(|trace| selected_trace.is_none_or(|selected| trace.name.value == selected))
        .map(|trace| analyze_trace(program, trace, options))
        .collect()
}

fn analyze_trace(
    program: &CompiledProgram,
    trace: &TraceDecl,
    options: &AnalysisOptions,
) -> TraceAnalysis {
    let bound = trace.within.value;
    let Some(state_decl) = program.state(&trace.variable.ty.value) else {
        return failed_without_path(
            trace,
            TraceCounterexampleKind::EvaluationConflict,
            format!("unknown state type `{}`", trace.variable.ty.value),
        );
    };
    let state_space = match enumerate_state_space(program, state_decl, options.max_evaluations) {
        Ok(states) => states,
        Err(reason) => {
            return TraceAnalysis {
                trace: trace.name.value.clone(),
                verdict: AnalysisVerdict::Inconclusive,
                bound,
                evaluated_states: 0,
                reachable_states: 0,
                completeness: TraceCompleteness::Truncated,
                counterexamples: Vec::new(),
                notes: vec![reason],
            };
        }
    };

    let mut evaluated_states = 0usize;
    let mut initial_nodes = Vec::new();
    for state in state_space {
        if !consume_budget(&mut evaluated_states, options.max_evaluations) {
            return truncated(trace, bound, evaluated_states, 0);
        }
        let evaluation = evaluate_trace_condition(program, trace, &state, &trace.initial);
        match evaluation.truth {
            TruthValue::True => initial_nodes.push(FrontierNode {
                path: vec![TraceStep {
                    depth: 0,
                    transition: None,
                    action: None,
                    state: state.clone(),
                }],
                state,
            }),
            TruthValue::False => {}
            TruthValue::Unknown | TruthValue::Conflict => {
                let reason = condition_failure("initially", &evaluation);
                return failed(
                    trace,
                    bound,
                    evaluated_states,
                    0,
                    TraceCounterexampleKind::InitialConflict,
                    reason,
                    vec![TraceStep {
                        depth: 0,
                        transition: None,
                        action: None,
                        state,
                    }],
                );
            }
        }
    }

    if initial_nodes.is_empty() {
        return failed(
            trace,
            bound,
            evaluated_states,
            0,
            TraceCounterexampleKind::NoInitialState,
            "the `initially` condition selects no state".into(),
            Vec::new(),
        );
    }

    initial_nodes.sort_by(|left, right| left.state.cmp(&right.state));
    let transitions = applicable_transitions(program, &trace.variable.ty.value);
    let mut frontier = initial_nodes;
    let mut reachable = BTreeSet::new();

    for depth in 0..=bound {
        let mut next = BTreeMap::<TraceState, FrontierNode>::new();
        for node in frontier {
            if !consume_budget(&mut evaluated_states, options.max_evaluations) {
                return truncated(trace, bound, evaluated_states, reachable.len());
            }
            reachable.insert(node.state.clone());

            for (index, condition) in trace.always.iter().enumerate() {
                let evaluation = evaluate_trace_condition(program, trace, &node.state, condition);
                if evaluation.truth != TruthValue::True {
                    return failed(
                        trace,
                        bound,
                        evaluated_states,
                        reachable.len(),
                        if evaluation.truth == TruthValue::False {
                            TraceCounterexampleKind::InvariantViolation
                        } else {
                            TraceCounterexampleKind::EvaluationConflict
                        },
                        condition_failure(&format!("always clause {}", index + 1), &evaluation),
                        node.path,
                    );
                }
            }

            let terminal = trace
                .terminal
                .as_ref()
                .map(|condition| evaluate_trace_condition(program, trace, &node.state, condition));
            match terminal.as_ref().map(|evaluation| evaluation.truth) {
                Some(TruthValue::True) => continue,
                Some(TruthValue::Unknown | TruthValue::Conflict) => {
                    return failed(
                        trace,
                        bound,
                        evaluated_states,
                        reachable.len(),
                        TraceCounterexampleKind::EvaluationConflict,
                        condition_failure("terminates when", terminal.as_ref().unwrap()),
                        node.path,
                    );
                }
                Some(TruthValue::False) | None => {}
            }

            if depth == bound && terminal.is_some() {
                return failed(
                    trace,
                    bound,
                    evaluated_states,
                    reachable.len(),
                    TraceCounterexampleKind::NonTermination,
                    format!("a reachable path is still non-terminal after {bound} steps"),
                    node.path,
                );
            }

            let inspect_successors = depth < bound || trace.no_dead_ends;
            if !inspect_successors {
                continue;
            }
            let successors = match successors(program, state_decl, &node, &transitions, depth) {
                Ok(successors) => successors,
                Err(counterexample) => {
                    return failed_with_counterexample(
                        trace,
                        bound,
                        evaluated_states,
                        reachable.len(),
                        counterexample,
                    );
                }
            };
            if successors.is_empty() {
                if trace.no_dead_ends {
                    return failed(
                        trace,
                        bound,
                        evaluated_states,
                        reachable.len(),
                        TraceCounterexampleKind::DeadEnd,
                        "a reachable non-terminal state has no applicable transition".into(),
                        node.path,
                    );
                }
                if terminal.is_some() {
                    return failed(
                        trace,
                        bound,
                        evaluated_states,
                        reachable.len(),
                        TraceCounterexampleKind::NonTermination,
                        "a reachable non-terminal state cannot reach a terminal state".into(),
                        node.path,
                    );
                }
            }
            if depth < bound {
                for successor in successors {
                    next.entry(successor.state.clone()).or_insert(successor);
                }
            }
        }
        if next.is_empty() {
            return passed(trace, bound, evaluated_states, reachable.len());
        }
        frontier = next.into_values().collect();
    }

    passed(trace, bound, evaluated_states, reachable.len())
}

fn successors(
    program: &CompiledProgram,
    state_decl: &crate::ast::StateDecl,
    node: &FrontierNode,
    transitions: &[&TransitionDecl],
    depth: usize,
) -> Result<Vec<FrontierNode>, TraceCounterexample> {
    let mut output = Vec::new();
    for transition in transitions {
        let input = state_input(state_decl, &node.state);
        let variables = BTreeMap::from([(
            transition.parameters[0].name.value.clone(),
            STATE_BINDING.to_owned(),
        )]);
        let condition =
            evaluate_condition(program, &input, variables.clone(), &transition.condition);
        match condition.truth {
            TruthValue::False => continue,
            TruthValue::Unknown | TruthValue::Conflict => {
                return Err(TraceCounterexample {
                    kind: TraceCounterexampleKind::EvaluationConflict,
                    reason: format!(
                        "transition `{}` condition could not be decided: {}",
                        transition.name.value,
                        condition_detail(&condition)
                    ),
                    path: node.path.clone(),
                    attempted: Some(trace_attempt(transition)),
                });
            }
            TruthValue::True => {}
        }

        let mut next_state = node.state.clone();
        for update in &transition.updates {
            let Some(field) = program.state_field(&state_decl.name.value, &update.field.value)
            else {
                return Err(TraceCounterexample {
                    kind: TraceCounterexampleKind::InvalidUpdate,
                    reason: format!(
                        "transition `{}` updates unknown field `{}`",
                        transition.name.value, update.field.value
                    ),
                    path: node.path.clone(),
                    attempted: Some(trace_attempt(transition)),
                });
            };
            let value = evaluate_value(
                program,
                &input,
                variables.clone(),
                &update.value,
                Some(&field.ty),
            );
            let value = match value {
                ValueEvaluation::Known(value) => value,
                ValueEvaluation::Unknown(missing) => {
                    return Err(TraceCounterexample {
                        kind: TraceCounterexampleKind::InvalidUpdate,
                        reason: format!(
                            "transition `{}` update `{}` is unknown: {}",
                            transition.name.value,
                            update.field.value,
                            missing.join(", ")
                        ),
                        path: node.path.clone(),
                        attempted: Some(trace_attempt(transition)),
                    });
                }
                ValueEvaluation::Conflict(reasons) => {
                    return Err(TraceCounterexample {
                        kind: TraceCounterexampleKind::InvalidUpdate,
                        reason: format!(
                            "transition `{}` update `{}` conflicts: {}",
                            transition.name.value,
                            update.field.value,
                            reasons.join("; ")
                        ),
                        path: node.path.clone(),
                        attempted: Some(trace_attempt(transition)),
                    });
                }
            };
            if let Err(reason) = validate_field_value(program, field, &value) {
                return Err(TraceCounterexample {
                    kind: TraceCounterexampleKind::InvalidUpdate,
                    reason: format!(
                        "transition `{}` produced invalid `{}`: {reason}",
                        transition.name.value, update.field.value
                    ),
                    path: node.path.clone(),
                    attempted: Some(trace_attempt(transition)),
                });
            }
            next_state
                .fields
                .insert(normalize_name(&field.name.value), value);
        }
        let mut path = node.path.clone();
        path.push(TraceStep {
            depth: depth + 1,
            transition: Some(transition.name.value.clone()),
            action: Some(transition.action.value.clone()),
            state: next_state.clone(),
        });
        output.push(FrontierNode {
            state: next_state,
            path,
        });
    }
    output.sort_by(|left, right| left.state.cmp(&right.state));
    Ok(output)
}

fn trace_attempt(transition: &TransitionDecl) -> TraceAttempt {
    TraceAttempt {
        transition: transition.name.value.clone(),
        action: transition.action.value.clone(),
    }
}

fn applicable_transitions<'a>(
    program: &'a CompiledProgram,
    state_name: &str,
) -> Vec<&'a TransitionDecl> {
    let state_name = normalize_name(state_name);
    program
        .transitions()
        .values()
        .filter(|transition| {
            transition.parameters.len() == 1
                && normalize_name(&transition.parameters[0].ty.value) == state_name
        })
        .collect()
}

fn evaluate_trace_condition(
    program: &CompiledProgram,
    trace: &TraceDecl,
    state: &TraceState,
    expression: &crate::ast::Expr,
) -> crate::engine::ConditionEvaluation {
    let state_decl = program
        .state(&trace.variable.ty.value)
        .expect("compiled trace state exists");
    let input = state_input(state_decl, state);
    evaluate_condition(
        program,
        &input,
        BTreeMap::from([(trace.variable.name.value.clone(), STATE_BINDING.to_owned())]),
        expression,
    )
}

fn state_input(state_decl: &crate::ast::StateDecl, state: &TraceState) -> Input {
    let mut input = Input::new();
    input.insert(
        STATE_BINDING,
        state_decl.name.value.clone(),
        state.fields.clone(),
    );
    input
}

fn enumerate_state_space(
    program: &CompiledProgram,
    state: &crate::ast::StateDecl,
    limit: usize,
) -> Result<Vec<TraceState>, String> {
    let mut fields = Vec::new();
    let mut size = 1usize;
    for field in &state.fields {
        let values = state_field_values(program, field)?;
        size = size
            .checked_mul(values.len())
            .ok_or_else(|| format!("state `{}` is too large to materialize", state.name.value))?;
        if size > limit {
            return Err(format!(
                "state `{}` has {size} combinations, exceeding the evaluation limit of {limit}",
                state.name.value
            ));
        }
        fields.push((normalize_name(&field.name.value), values));
    }
    let mut output = Vec::with_capacity(size);
    enumerate_product(&fields, 0, &mut BTreeMap::new(), &mut output);
    Ok(output)
}

fn state_field_values(program: &CompiledProgram, field: &FieldDecl) -> Result<Vec<Value>, String> {
    match &field.ty {
        TypeRef::Bool => Ok(vec![Value::Bool(false), Value::Bool(true)]),
        TypeRef::Int => {
            let range = field
                .range
                .as_ref()
                .ok_or_else(|| format!("state Int field `{}` has no range", field.name.value))?;
            let NumericLiteral::Int(start) = range.start else {
                return Err(format!(
                    "state Int field `{}` has a non-Int range",
                    field.name.value
                ));
            };
            let NumericLiteral::Int(end) = range.end else {
                return Err(format!(
                    "state Int field `{}` has a non-Int range",
                    field.name.value
                ));
            };
            let capacity = i128::from(end) - i128::from(start) + 1;
            let capacity = usize::try_from(capacity).map_err(|_| {
                format!("state Int field `{}` range is too large", field.name.value)
            })?;
            let mut values = Vec::with_capacity(capacity);
            let mut value = start;
            loop {
                values.push(Value::Int(value));
                if value == end {
                    break;
                }
                value = value.checked_add(1).ok_or_else(|| {
                    format!("state Int field `{}` range overflows", field.name.value)
                })?;
            }
            Ok(values)
        }
        TypeRef::Named(enum_name) => {
            let declaration = program.enum_decl(enum_name).ok_or_else(|| {
                format!(
                    "state field `{}` references unknown enum `{enum_name}`",
                    field.name.value
                )
            })?;
            Ok(declaration
                .variants
                .iter()
                .map(|variant| Value::Enum {
                    type_name: normalize_name(enum_name),
                    variant: normalize_name(&variant.value),
                })
                .collect())
        }
        _ => Err(format!(
            "state field `{}` does not have a finite supported type",
            field.name.value
        )),
    }
}

fn enumerate_product(
    fields: &[(String, Vec<Value>)],
    index: usize,
    current: &mut BTreeMap<String, Value>,
    output: &mut Vec<TraceState>,
) {
    let Some((name, values)) = fields.get(index) else {
        output.push(TraceState {
            fields: current.clone(),
        });
        return;
    };
    for value in values {
        current.insert(name.clone(), value.clone());
        enumerate_product(fields, index + 1, current, output);
    }
    current.remove(name);
}

fn consume_budget(evaluated: &mut usize, limit: usize) -> bool {
    if *evaluated >= limit {
        false
    } else {
        *evaluated += 1;
        true
    }
}

fn condition_detail(evaluation: &crate::engine::ConditionEvaluation) -> String {
    if !evaluation.reasons.is_empty() {
        evaluation.reasons.join("; ")
    } else if !evaluation.missing.is_empty() {
        format!("missing {}", evaluation.missing.join(", "))
    } else {
        format!("evaluated to {:?}", evaluation.truth)
    }
}

fn condition_failure(clause: &str, evaluation: &crate::engine::ConditionEvaluation) -> String {
    match evaluation.truth {
        TruthValue::False => format!("{clause} evaluated to false"),
        TruthValue::Unknown | TruthValue::Conflict => {
            format!(
                "{clause} could not be decided: {}",
                condition_detail(evaluation)
            )
        }
        TruthValue::True => format!("{clause} unexpectedly failed"),
    }
}

fn failed_without_path(
    trace: &TraceDecl,
    kind: TraceCounterexampleKind,
    reason: String,
) -> TraceAnalysis {
    failed(trace, trace.within.value, 0, 0, kind, reason, Vec::new())
}

fn failed(
    trace: &TraceDecl,
    bound: usize,
    evaluated_states: usize,
    reachable_states: usize,
    kind: TraceCounterexampleKind,
    reason: String,
    path: Vec<TraceStep>,
) -> TraceAnalysis {
    TraceAnalysis {
        trace: trace.name.value.clone(),
        verdict: AnalysisVerdict::Failed,
        bound,
        evaluated_states,
        reachable_states,
        completeness: TraceCompleteness::BoundedExhaustive,
        counterexamples: vec![TraceCounterexample {
            kind,
            reason,
            path,
            attempted: None,
        }],
        notes: Vec::new(),
    }
}

fn failed_with_counterexample(
    trace: &TraceDecl,
    bound: usize,
    evaluated_states: usize,
    reachable_states: usize,
    counterexample: TraceCounterexample,
) -> TraceAnalysis {
    TraceAnalysis {
        trace: trace.name.value.clone(),
        verdict: AnalysisVerdict::Failed,
        bound,
        evaluated_states,
        reachable_states,
        completeness: TraceCompleteness::BoundedExhaustive,
        counterexamples: vec![counterexample],
        notes: Vec::new(),
    }
}

fn passed(
    trace: &TraceDecl,
    bound: usize,
    evaluated_states: usize,
    reachable_states: usize,
) -> TraceAnalysis {
    TraceAnalysis {
        trace: trace.name.value.clone(),
        verdict: AnalysisVerdict::Passed,
        bound,
        evaluated_states,
        reachable_states,
        completeness: TraceCompleteness::BoundedExhaustive,
        counterexamples: Vec::new(),
        notes: Vec::new(),
    }
}

fn truncated(
    trace: &TraceDecl,
    bound: usize,
    evaluated_states: usize,
    reachable_states: usize,
) -> TraceAnalysis {
    TraceAnalysis {
        trace: trace.name.value.clone(),
        verdict: AnalysisVerdict::Inconclusive,
        bound,
        evaluated_states,
        reachable_states,
        completeness: TraceCompleteness::Truncated,
        counterexamples: Vec::new(),
        notes: vec![format!(
            "stopped at the configured evaluation limit after {evaluated_states} state visits"
        )],
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::SourceFile;

    fn compile(text: &str) -> CompiledProgram {
        let output = crate::compile_source(SourceFile::new("trace.tes", text));
        assert!(
            !output
                .diagnostics
                .iter()
                .any(|diagnostic| diagnostic.severity == crate::Severity::Error),
            "{:?}",
            output.diagnostics
        );
        output.program.unwrap()
    }

    #[test]
    fn proves_termination_and_safety_over_all_reachable_states() {
        let program = compile(
            r"mod lights
enum Phase:
    Red
    Green

state Light:
    phase: Phase
    ticks: Int 0..2

action advance(light Light)

transition tick(light Light) on advance(light):
    when light.ticks < 2
    set light.ticks = light.ticks + 1

transition finish(light Light) on advance(light):
    when light.ticks = 2
    set light.phase = Green

trace reaches_green(light Light):
    initially light.phase = Red and light.ticks = 0
    always light.ticks >= 0
    terminates when light.phase = Green
    no dead ends
    within 3 steps
",
        );
        let traces = analyze_traces(&program, None, &AnalysisOptions::default());
        assert_eq!(traces.len(), 1);
        assert_eq!(traces[0].verdict, AnalysisVerdict::Passed);
        assert_eq!(traces[0].completeness, TraceCompleteness::BoundedExhaustive);
        assert_eq!(traces[0].reachable_states, 4);
    }

    #[test]
    fn returns_a_stable_shortest_safety_counterexample() {
        let program = compile(
            r"mod counter
state Counter:
    count: Int 0..2

action increment(counter Counter)

transition increment_once(counter Counter) on increment(counter):
    when counter.count < 2
    set counter.count = counter.count + 1

trace stays_small(counter Counter):
    initially counter.count = 0
    always counter.count < 2
    within 3 steps
",
        );
        let first = analyze_traces(&program, None, &AnalysisOptions::default());
        let second = analyze_traces(&program, None, &AnalysisOptions::default());
        assert_eq!(
            serde_json::to_value(&first).unwrap(),
            serde_json::to_value(&second).unwrap()
        );
        let counterexample = &first[0].counterexamples[0];
        assert_eq!(
            counterexample.kind,
            TraceCounterexampleKind::InvariantViolation
        );
        assert_eq!(counterexample.path.len(), 3);
        assert_eq!(counterexample.path[2].state.fields["count"], Value::Int(2));
    }

    #[test]
    fn distinguishes_dead_ends_invalid_updates_and_bounded_nontermination() {
        let dead_end = compile(
            r"mod stopped
state Machine:
    running: Bool

trace cannot_stall(machine Machine):
    initially not machine.running
    no dead ends
    within 2 steps
",
        );
        let analysis = analyze_traces(&dead_end, None, &AnalysisOptions::default());
        assert_eq!(
            analysis[0].counterexamples[0].kind,
            TraceCounterexampleKind::DeadEnd
        );

        let invalid = compile(
            r"mod overflow
state Counter:
    count: Int 0..1

action increment(counter Counter)

transition too_far(counter Counter) on increment(counter):
    when true
    set counter.count = counter.count + 1

trace bounded_counter(counter Counter):
    initially counter.count = 0
    always true
    within 2 steps
",
        );
        let analysis = analyze_traces(&invalid, None, &AnalysisOptions::default());
        let invalid_counterexample = &analysis[0].counterexamples[0];
        assert_eq!(
            invalid_counterexample.kind,
            TraceCounterexampleKind::InvalidUpdate
        );
        assert_eq!(
            invalid_counterexample.attempted,
            Some(TraceAttempt {
                transition: "too_far".into(),
                action: "increment".into(),
            })
        );
        assert_eq!(invalid_counterexample.path.len(), 2);
        assert_eq!(
            invalid_counterexample.path[1].state.fields["count"],
            Value::Int(1)
        );
        assert!(
            analysis[0]
                .render_text()
                .contains("attempted · increment / too_far")
        );

        let looping = compile(
            r"mod looping
state Machine:
    done: Bool

action wait(machine Machine)

transition wait_again(machine Machine) on wait(machine):
    when not machine.done
    set machine.done = false

trace must_finish(machine Machine):
    initially not machine.done
    terminates when machine.done
    within 2 steps
",
        );
        let analysis = analyze_traces(&looping, None, &AnalysisOptions::default());
        let counterexample = &analysis[0].counterexamples[0];
        assert_eq!(counterexample.kind, TraceCounterexampleKind::NonTermination);
        assert_eq!(counterexample.path.len(), 3);
    }
}