eq.rs

#![allow(non_snake_case)]
#![no_main]

extern crate klee;
use klee::{kassert, ksymbol,kassume};

#[no_mangle]
fn main() {
    let mut DATA: [Data; (DISCREPENCY + 2) as usize] =
        unsafe { core::mem::uninitialized() };
    ksymbol!(&mut DATA, "DATA");

    let mut STATE_HISTORY: [State; (DISCREPENCY + 2) as usize] =
        unsafe { core::mem::uninitialized() };

    let mut TIMEOUT_CNTR: u32 = 0;
    let mut STATE = S8001;

    for i in 0..(DISCREPENCY + 2) as usize {
        periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);

        // invariants
        // S8000 -> a & b
        // ensures that both inputs are true if we are in the Enable state S8000
        if STATE == S8000 {
            kassert!(DATA[i].a & DATA[i].b);
        }
        // !a | !b -> ! S8000
        // ensures that if any input is true we cannot be in the Enable state
        if !DATA[i].a | !DATA[i].b {
            kassert!(!(STATE == S8000));
        }
        // S8001 -> !a & !b
        // we can only stay or enter the Init state if both inputs are false
        if STATE == S8001 {
            kassert!(!DATA[i].a | !DATA[i].b);
        }
        // !a & !b -> S8001
        // ensures that we enter the Init state if both inputs are false
        if !DATA[i].a & !DATA[i].b & (TIMEOUT_CNTR > 0) {
            kassert!(STATE == S8001);
        }

        // DISCREPANCY relatod invariants
        match STATE {
            // error states implies TIMEOUT_CNTR to have expired
            C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
            // wait states implies that TIMEOUT_CNTR not yet expired
            S8004 | S8005 | S8014 => {
                kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY)
            }
            _ => {}
        }

        // transition invariants
        if i > 0 {
            match STATE_HISTORY[i - 1] {
                C001 | C002 | C003 | S8005 => {
                    // no (immediate) transition from error / recover to Enable state
                   kassert!(!(STATE == S8000));
                }
                _ => {
                    // liveness from Init and Wait states, Enable ensured
                    if DATA[i].a & DATA[i].b  & (TIMEOUT_CNTR > 0) {
                        kassert!(STATE == S8000);
                    }
                }
            }
        }
        STATE_HISTORY[i] = STATE;
    }
}

#[derive(Debug, Copy, Clone)]
pub struct Data {
    a: bool,
    b: bool,
}

#[derive(Debug, Copy, Clone, PartialEq)]
pub enum State {
    S8000,
    S8001,
    S8004,
    S8014,
    S8005,
    C001,
    C002,
    C003,
}

use State::*;

const DISCREPENCY: u32 = 3;
const T: bool = true;
const F: bool = false;

fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
    // we start directly in the init state S80001
    // static mut STATE: State = State::S8001;
    // static mut TIMEOUT_CNTR: u32 = 0;

    let data = DATA;

    *STATE = match STATE {
        S8000 => match (data.a, data.b) {
            (F, F) => S8001,
            (F, T) | (T, F) => {
                *TIMEOUT_CNTR = DISCREPENCY;
                S8005
            }
            (T, T) => S8000,
        },
        S8001 => match (data.a, data.b) {
            (F, F) => S8001,
            (F, T) => {
                *TIMEOUT_CNTR = DISCREPENCY;
                S8014
            }
            (T, F) => {
                *TIMEOUT_CNTR = DISCREPENCY;
                S8004
            }
            (T, T) => S8000,
        },
        S8004 => {
            *TIMEOUT_CNTR -= 1;
            match *TIMEOUT_CNTR {
                0 => C001,
                _ => match (data.a, data.b) {
                    (F, _) => S8001,
                    (_, T) => S8000,
                    _ => S8004,
                },
            }
        }
        S8014 => {
            *TIMEOUT_CNTR -= 1;
            match *TIMEOUT_CNTR {
                0 => C002,
                _ => match (data.a, data.b) {
                    (_, F) => S8001,
                    (T, _) => S8000,
                    _ => S8014,
                },
            }
        }
        S8005 => {
            *TIMEOUT_CNTR -= 1;
            match *TIMEOUT_CNTR {
                0 => C003,
                _ => match (data.a, data.b) {
                    (F, F) => S8001,
                    _ => S8005,
                },
            }
        }
        C001 | C002 => match (data.a, data.b) {
            (F, F) => S8001,
            _ => *STATE,
        },
        C003 => match (data.a, data.b) {
            (F, F) => S8001,
            _ => C003,
        },
    };
}