rust_formal_verification/models/finite_state_transition_system/
getting.rs

1// ************************************************************************************************
2// use
3// ************************************************************************************************
4
5use crate::formulas::literal::VariableType;
6use crate::formulas::{Clause, Cube, CNF};
7
8use super::FiniteStateTransitionSystem;
9
10// ************************************************************************************************
11// impl
12// ************************************************************************************************
13
14impl FiniteStateTransitionSystem {
15    // ********************************************************************************************
16    // aig api functions
17    // ********************************************************************************************
18
19    pub fn get_max_literal_number(&self) -> VariableType {
20        self.max_literal_number
21    }
22
23    pub fn get_state_literal_numbers(&self) -> Vec<VariableType> {
24        self.state_literals.to_owned()
25    }
26
27    pub fn get_input_literal_numbers(&self) -> Vec<VariableType> {
28        self.input_literals.to_owned()
29    }
30
31    pub fn get_initial_relation(&self) -> Cube {
32        self.initial_states.to_owned()
33    }
34
35    /// Function that gets the transition relation for the FiniteStateTransitionSystem.
36    ///
37    /// # Arguments
38    ///
39    /// * `self: &FiniteStateTransitionSystem` - the FiniteStateTransitionSystem desired.
40    ///
41    /// # Examples
42    /// ```
43    /// use rust_formal_verification::models::{AndInverterGraph, FiniteStateTransitionSystem};
44    /// use rust_formal_verification::formulas::CNF;
45    /// let file_path = "tests/examples/ours/counter.aig";
46    /// let aig = AndInverterGraph::from_aig_path(file_path);
47    /// let fsts = FiniteStateTransitionSystem::from_aig(&aig, false);
48    /// let mut tr_x_x_tag = CNF::default();
49    /// let tr_x_x_tag = fsts.get_transition_relation();
50    /// assert_eq!(
51    ///     tr_x_x_tag.to_string(),
52    ///     "p cnf 8 12\n1 -7 0\n-1 -5 0\n-1 7 0\n2 -8 0\n-2 -4 0\n-2 8 0\n-3 -4 0\n4 -5 0\n5 -6 0\n-5 6 0\n1 -4 5 0\n2 3 4 0"
53    /// );
54    /// ```
55    pub fn get_transition_relation(&self) -> CNF {
56        self.transition.to_owned()
57    }
58
59    pub fn get_state_to_safety_translation(&self) -> CNF {
60        self.state_to_safety_translation.to_owned()
61    }
62
63    pub fn get_safety_property(&self) -> Cube {
64        !self.unsafety_property.to_owned()
65    }
66
67    pub fn get_unsafety_property(&self) -> Clause {
68        self.unsafety_property.to_owned()
69    }
70}
rust_formal_verification/models/finite_state_transition_system/getting.rs

rust_formal_verification/models/finite_state_transition_system/
getting.rs
