use mirrorrust::{run_client, get_param, as_int, ApalacheConfig, State, StateComputer, TraceGenerationConfig, Value};
use num_bigint::BigInt;

struct Counter { count: BigInt }
impl StateComputer for Counter {
    fn compute(&mut self, action: &str, params: &State, prev: &State) -> State {
        if action == "Init" || !prev.contains_key("count") {
            self.count = BigInt::from(0);
        } else {
            let stride = get_param(params, "parameters")
                .and_then(|r| r.get("stride")).and_then(as_int).cloned()
                .unwrap_or_else(|| BigInt::from(0));
            self.count += stride;
        }
        [("count".to_string(), Value::Int(self.count.clone()))].into_iter().collect()
    }
}

fn main() -> Result<(), mirrorrust::Error> {
    run_client(
        "/path/to/ModelMirros",
        ApalacheConfig {
            spec_path: "specs/Counter.tla".into(),
            invariant: "TraceComplete".into(),
            length_bound: 6,
            const_init: Some("CInit".into()),
            param_vars: Some("parameters".into()),
            init_predicate: None,
            next_predicate: None,
        },
        TraceGenerationConfig { num_traces: 100, view: Some("View".into()) },
        Counter { count: BigInt::from(0) },
    )
}