holos_tda/coverage_synthesis/
types.rs

1//! Coverage actions, evaluations, and status values.
2
3use std::fmt;
4
5use crate::{Error, Result};
6
7use super::specification::CoverageSpecification;
8
9/// One candidate sensor activation and the states where it is available.
10#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
11pub struct CoverageAction {
12    /// Sensor vertex activated by this action.
13    pub vertex: usize,
14    /// Positive additive action cost.
15    pub cost: u64,
16    pub(crate) states: Vec<usize>,
17}
18
19impl CoverageAction {
20    /// Construct an activation and canonicalize its affected states.
21    pub fn new(vertex: usize, cost: u64, mut states: Vec<usize>) -> Self {
22        states.sort_unstable();
23        states.dedup();
24        Self {
25            vertex,
26            cost,
27            states,
28        }
29    }
30
31    /// State indices where this sensor is activated.
32    pub fn states(&self) -> &[usize] {
33        &self.states
34    }
35
36    /// Construct an activation that applies to every state.
37    pub fn throughout(vertex: usize, cost: u64, specification: &CoverageSpecification) -> Self {
38        Self::new(vertex, cost, (0..specification.states.len()).collect())
39    }
40}
41
42/// One independent state-action incidence component.
43#[derive(Debug, Clone, Default, PartialEq, Eq)]
44pub struct CoverageComponent {
45    pub(crate) states: Vec<usize>,
46    pub(crate) actions: Vec<usize>,
47}
48
49impl CoverageComponent {
50    /// State indices in this component.
51    pub fn states(&self) -> &[usize] {
52        &self.states
53    }
54
55    /// Action indices in this component.
56    pub fn actions(&self) -> &[usize] {
57        &self.actions
58    }
59}
60
61/// First state and failure set that refutes a selected plan.
62#[derive(Debug, Clone, PartialEq, Eq)]
63pub struct CoverageCounterexample {
64    /// State index in the canonical specification.
65    pub state: usize,
66    /// Failed sensor vertices in ascending order.
67    pub failed_vertices: Vec<usize>,
68}
69
70/// Exact result of evaluating one selected activation set.
71#[derive(Debug, Clone, PartialEq, Eq)]
72pub struct CoveragePlanEvaluation {
73    /// True when every state survives every allowed failure.
74    pub criterion_holds: bool,
75    /// Number of state and maximal-failure pairs checked.
76    pub checks: usize,
77    /// Smallest witness support among accepted checks.
78    pub minimum_witness_triangles: Option<usize>,
79    /// First canonical failed check, when one exists.
80    pub counterexample: Option<CoverageCounterexample>,
81}
82
83/// Completeness status of a coverage synthesis result.
84#[derive(Debug, Clone, Copy, PartialEq, Eq)]
85pub enum CoverageSynthesisStatus {
86    /// The selected activations have minimum total cost.
87    Optimal,
88    /// No plan within the activation limit satisfies the specification.
89    Infeasible,
90    /// A producer work limit stopped search before a complete proof.
91    SearchIncomplete,
92}
93
94impl CoverageSynthesisStatus {
95    pub(crate) fn code(self) -> u8 {
96        match self {
97            Self::Optimal => 1,
98            Self::Infeasible => 2,
99            Self::SearchIncomplete => 3,
100        }
101    }
102
103    pub(crate) fn from_code(code: u8) -> Result<Self> {
104        match code {
105            1 => Ok(Self::Optimal),
106            2 => Ok(Self::Infeasible),
107            3 => Ok(Self::SearchIncomplete),
108            _ => Err(Error::InvalidInput(
109                "coverage synthesis status is invalid".into(),
110            )),
111        }
112    }
113}
114
115impl fmt::Display for CoverageSynthesisStatus {
116    fn fmt(&self, formatter: &mut fmt::Formatter<'_>) -> fmt::Result {
117        formatter.write_str(match self {
118            Self::Optimal => "optimal",
119            Self::Infeasible => "infeasible",
120            Self::SearchIncomplete => "search incomplete",
121        })
122    }
123}
124
125#[derive(Debug, Clone, Copy, PartialEq, Eq)]
126pub(crate) struct EvaluationClaim {
127    pub(crate) criterion_holds: bool,
128    pub(crate) checks: usize,
129    pub(crate) minimum_witness_triangles: Option<usize>,
130}
131
132impl From<&CoveragePlanEvaluation> for EvaluationClaim {
133    fn from(evaluation: &CoveragePlanEvaluation) -> Self {
134        Self {
135            criterion_holds: evaluation.criterion_holds,
136            checks: evaluation.checks,
137            minimum_witness_triangles: evaluation.minimum_witness_triangles,
138        }
139    }
140}
holos_tda/coverage_synthesis/types.rs

holos_tda/coverage_synthesis/
types.rs
