libpetri_verification/
environment.rs

1/// How environment places should be treated during verification.
2/// Controls how environment places (external event sources) are treated
3/// during formal analysis.
4#[derive(Debug, Clone, PartialEq, Eq)]
5pub enum EnvironmentAnalysisMode {
6    /// Environment places are always considered to have tokens available.
7    /// Transitions reading from environment places are always enabled.
8    AlwaysAvailable,
9    /// Environment places are treated as having at most `max_tokens` tokens.
10    /// Explores states where 0..=max_tokens tokens are injected.
11    Bounded { max_tokens: usize },
12    /// Environment places are treated as regular places (no special handling).
13    Ignore,
14}
15
16/// Creates an `AlwaysAvailable` environment mode.
17pub fn always_available() -> EnvironmentAnalysisMode {
18    EnvironmentAnalysisMode::AlwaysAvailable
19}
20
21/// Creates a `Bounded` environment mode with the given max token count.
22pub fn bounded(max_tokens: usize) -> EnvironmentAnalysisMode {
23    EnvironmentAnalysisMode::Bounded { max_tokens }
24}
25
26/// Creates an `Ignore` environment mode (treats env places as regular).
27pub fn ignore() -> EnvironmentAnalysisMode {
28    EnvironmentAnalysisMode::Ignore
29}
30
31#[cfg(test)]
32mod tests {
33    use super::*;
34
35    #[test]
36    fn mode_constructors() {
37        assert_eq!(always_available(), EnvironmentAnalysisMode::AlwaysAvailable);
38        assert_eq!(
39            bounded(3),
40            EnvironmentAnalysisMode::Bounded { max_tokens: 3 }
41        );
42        assert_eq!(ignore(), EnvironmentAnalysisMode::Ignore);
43    }
44}
libpetri_verification/environment.rs

libpetri_verification/
environment.rs
