rust_formal_verification/models/finite_state_transition_system/
mod.rs

1//! Object for holding a finite state transition system, and performing operations like adding
2//! tags and so on.
3
4// ************************************************************************************************
5// use
6// ************************************************************************************************
7
8use crate::formulas::{literal::VariableType, Clause, Cube, Literal, CNF};
9use std::collections::{HashMap, HashSet};
10
11use super::and_inverter_graph::AIGWire;
12
13// ************************************************************************************************
14// struct
15// ************************************************************************************************
16
17/// Struct that describes memory layout of the finite state transition system.
18///
19/// implementations of many additional features can be found in sub-modules.
20#[derive(Clone)]
21pub struct FiniteStateTransitionSystem {
22    initial_literals: HashSet<Literal>,
23    initial_states: Cube,
24    transition: CNF,
25    state_to_safety_translation: CNF,
26    unsafety_property: Clause,
27    max_literal_number: VariableType,
28    state_literals: Vec<VariableType>,
29    input_literals: Vec<VariableType>,
30    cone_of_safety_only_latches: HashSet<VariableType>,
31    cone_of_transition_only_latches: HashSet<VariableType>,
32    bad_wires: Vec<AIGWire>,
33    wire_mappings_from_latch_to_latch_input: HashMap<AIGWire, AIGWire>,
34    and_information_in_cone_of_bad_sorted_by_output: Vec<(AIGWire, AIGWire, AIGWire)>,
35    and_information_in_cone_of_transition_sorted_by_output: Vec<(AIGWire, AIGWire, AIGWire)>,
36}
37
38// ************************************************************************************************
39// rust submodule declaration, they get searched in their respective file  names
40// ************************************************************************************************
41
42pub mod construction;
43pub mod features;
44pub mod getting;
45pub mod x_simulation;
46
47// ************************************************************************************************
48// re-exports of structs in these modules to simplify paths for other imports
49// ************************************************************************************************
rust_formal_verification/models/finite_state_transition_system/mod.rs

rust_formal_verification/models/finite_state_transition_system/
mod.rs
