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

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

#[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 DISCREPANCY: u32 = 1;
const HORIZON: usize = (DISCREPANCY + 4) as usize;
const T: bool = true;
const F: bool = false;

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

  let mut STATE_H: [State; HORIZON] =
    unsafe { core::mem::uninitialized() };

  let mut CNTR_H: [u32; HORIZON] =
    unsafe { core::mem::uninitialized() };

  let mut TIMEOUT_CNTR: u32 =
    unsafe { core::mem::uninitialized() };
  let mut STATE = S8001;

  for i in 0..HORIZON {
    eq(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
    STATE_H[i] = STATE;
    CNTR_H[i] = TIMEOUT_CNTR;

    // (1) !a | !b -> !S8000
    // ensures that if any input is false we cannot enter the Enable state
    // this can also be seen as a safty condition
    // (can it be derived from the first condition, but we keep is as
    // an indication that the verification works as expected)
    // Indeed the number of spanned paths remains the same
    // (with or without the below assertion, so its proven redundant by KLEE)
    if !DATA[i].a | !DATA[i].b {
      kassert!(!(STATE == S8000));
    }

    // invariants
    // (2) S8000 -> a & b
    // ensures that Enable implies that both a and b are true
    // this is the main safety condition
    if STATE == S8000 {
      kassert!(DATA[i].a & DATA[i].b);
    }

    // transition invariants
    if i > 0 {
      match STATE_H[i - 1] {
        C001 | C002 | C003 => {
          // (3)
          // transitions from error
          kassert!(
            (STATE_H[i] == S8001)
              | (STATE == STATE_H[i - 1])
          );
        }
        S8005 => {
          // (4)
          kassert!(
            (STATE_H[i] == S8001)
              | (STATE == C003)
              | (STATE == STATE_H[i - 1])
          );
        }
        _ => (),
      }
    }

    // // DISCREPANCY related invariants
    match STATE {
      // Error -> timeout
      // (5)
      C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),

      S8004 | S8005 | S8014 => {
        // (6)
        // remaining in a waiting state decreases the counter
        if i > 0 {
          if STATE_H[i - 1] == STATE_H[i] {
            kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]);
          }
        }
      }
      _ => {}
    }
  }
}

fn eq(
  STATE: &mut State,
  TIMEOUT_CNTR: &mut u32,
  data: &Data,
) {
  *STATE = match STATE {
    S8000 => match (data.a, data.b) {
      (F, F) => S8001,
      (F, T) | (T, F) => {
        *TIMEOUT_CNTR = DISCREPANCY;
        S8005
      }
      (T, T) => S8000,
    },
    S8001 => match (data.a, data.b) {
      (F, F) => S8001,
      (F, T) => {
        *TIMEOUT_CNTR = DISCREPANCY;
        S8014
      }
      (T, F) => {
        *TIMEOUT_CNTR = DISCREPANCY;
        S8004
      }
      (T, T) => S8000,
    },
    S8004 => match *TIMEOUT_CNTR {
      0 => C001,
      _ => {
        *TIMEOUT_CNTR -= 1;
        match (data.a, data.b) {
          (F, _) => S8001,
          (_, T) => S8000,
          _ => S8004,
        }
      }
    },
    S8014 => match *TIMEOUT_CNTR {
      0 => C002,
      _ => {
        *TIMEOUT_CNTR -= 1;
        match (data.a, data.b) {
          (_, F) => S8001,
          (T, _) => S8000,
          _ => S8014,
        }
      }
    },
    S8005 => match *TIMEOUT_CNTR {
      0 => C003,
      _ => {
        *TIMEOUT_CNTR -= 1;
        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,
    },
  };
}