Struct FiniteStateTransitionSystem 

pub struct FiniteStateTransitionSystem { /* private fields */ }

Struct that describes memory layout of the finite state transition system.

implementations of many additional features can be found in sub-modules.

Implementations

impl FiniteStateTransitionSystem

pub fn from_aig(aig: &AndInverterGraph, assume_output_is_bad: bool) -> Self

Function that converts an AndInverterGraph into a FiniteStateTransitionSystem.

Arguments

• aig: &AndInverterGraph - the AndInverterGraph desired.

Examples

use rust_formal_verification::models::{AndInverterGraph, FiniteStateTransitionSystem};
let file_path = "tests/examples/ours/counter.aig";
let aig = AndInverterGraph::from_aig_path(file_path);
let fsts = FiniteStateTransitionSystem::from_aig(&aig, false);
assert_eq!(fsts.get_initial_relation().to_string(), "p cnf 3 3\n-1 0\n-2 0\n-3 0");

impl FiniteStateTransitionSystem

pub fn add_tags_to_relation( &self, relation: &CNF, number_of_tags: VariableType, ) -> CNF

pub fn add_tags_to_cube( &self, cube: &Cube, number_of_tags: VariableType, ) -> Cube

pub fn add_tags_to_clause( &self, clause: &Clause, number_of_tags: VariableType, ) -> Clause

pub fn is_cube_initial(&self, cube: &Cube) -> bool

pub fn extract_state_from_assignment(&self, assignment: &Assignment) -> Cube

pub fn extract_input_from_assignment(&self, assignment: &Assignment) -> Cube

pub fn intersect_cube_with_cone_of_safety(&self, c: &Cube) -> Cube

pub fn intersect_cube_with_cone_of_transition(&self, c: &Cube) -> Cube

pub fn check_invariant<T: StatelessSatSolver>(&self, inv_candidate: &CNF)

impl FiniteStateTransitionSystem

pub fn get_max_literal_number(&self) -> VariableType

pub fn get_state_literal_numbers(&self) -> Vec<VariableType>

pub fn get_input_literal_numbers(&self) -> Vec<VariableType>

pub fn get_initial_relation(&self) -> Cube

pub fn get_transition_relation(&self) -> CNF

Function that gets the transition relation for the FiniteStateTransitionSystem.

Arguments

• self: &FiniteStateTransitionSystem - the FiniteStateTransitionSystem desired.

Examples

use rust_formal_verification::models::{AndInverterGraph, FiniteStateTransitionSystem};
use rust_formal_verification::formulas::CNF;
let file_path = "tests/examples/ours/counter.aig";
let aig = AndInverterGraph::from_aig_path(file_path);
let fsts = FiniteStateTransitionSystem::from_aig(&aig, false);
let mut tr_x_x_tag = CNF::default();
let tr_x_x_tag = fsts.get_transition_relation();
assert_eq!(
    tr_x_x_tag.to_string(),
    "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"
);

pub fn get_state_to_safety_translation(&self) -> CNF

pub fn get_safety_property(&self) -> Cube

pub fn get_unsafety_property(&self) -> Clause

impl FiniteStateTransitionSystem

pub fn simplify_unsafe_cube_using_trinary_simulation( &self, cube: &Cube, input: &Cube, rng: &mut ThreadRng, ) -> Cube

pub fn simplify_predecessor_cube_using_trinary_simulation( &self, predecessor_cube: &Cube, successor_cube: &Cube, input: &Cube, rng: &mut ThreadRng, ) -> Cube

Trait Implementations

impl Clone for FiniteStateTransitionSystem

fn clone(&self) -> FiniteStateTransitionSystem

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.