use std::collections::HashMap;
use std::path::Path;

use approx::assert_abs_diff_eq;
use csv::Reader;
use logic::expressions::{Bound, Predicate};
use logic::operators::{Always, And, Eventually, Implies, Next, Not, Or};
use logic::{Metric, Trace};

const SIG_FIGS: f64 = 1e-3;

fn p1() -> Predicate {
    Predicate::new(HashMap::from([("x".to_string(), -1.0)]), Bound::Constant(2.0))
}

fn p2() -> Predicate {
    Predicate::new(HashMap::from([("x".to_string(), 1.0)]), Bound::Constant(2.0))
}

fn load_test_trace() -> Trace<HashMap<String, f64>> {
    let file_name = file!();
    let tests_dir = Path::new(file_name).parent().unwrap();
    let data_file_path = tests_dir.join("trace_data.csv");

    let mut reader = Reader::from_path(data_file_path).unwrap();
    let timed_states = reader.records().into_iter().map(|result| {
        let record = result.unwrap();
        let time = record[0].parse().unwrap();
        let state = HashMap::from([("x".to_string(), record[1].parse().unwrap())]);

        (time, state)
    });

    Trace::from_iter(timed_states)
}

#[test]
fn case01() {
    let trace = load_test_trace();
    let formula = Or::new(p1(), p2());
    let distance = formula.distance(&trace);

    assert_eq!(distance.unwrap(), 2.0);
}

#[test]
fn case02() {
    let trace = load_test_trace();
    let formula = Eventually::new(p1());
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 3.7508, epsilon = SIG_FIGS);
}

#[test]
fn case03() {
    let trace = load_test_trace();
    let formula = Always::new(p2());
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 0.24923, epsilon = SIG_FIGS);
}

#[test]
fn case04() {
    let trace = load_test_trace();
    let formula = Next::new(p1());
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 2.5881, epsilon = SIG_FIGS);
}

#[test]
fn case05() {
    let trace = load_test_trace();
    let formula = Next::new(Next::new(p1()));
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 3.1068, epsilon = SIG_FIGS);
}

#[test]
fn case06() {
    let trace = load_test_trace();
    let formula = Next::new(Next::new(Next::new(p1())));
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 3.4967, epsilon = SIG_FIGS);
}

#[test]
fn case07() {
    let trace = load_test_trace();
    let formula = Always::new(Eventually::new(And::new(p2(), Eventually::new(p1()))));
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 1.184, epsilon = SIG_FIGS);
}

#[test]
fn case08() {
    let trace = load_test_trace();
    let formula = Implies::new(p1(), p2());
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 2.0, epsilon = SIG_FIGS);
}

#[test]
fn case09() {
    let trace = load_test_trace();
    let formula = And::new(Eventually::new(p1()), Always::new(Implies::new(p1(), Eventually::new(p2()))));
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 2.816, epsilon = SIG_FIGS);
}

#[test]
fn case10() {
    let trace = load_test_trace();
    let formula = Always::new(Implies::new(p1(), Eventually::new(Not::new(p1()))));
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), -1.184, epsilon = SIG_FIGS);
}

#[test]
fn case11() {
    let trace = load_test_trace();
    let formula = Always::new(Or::new(Not::new(p1()), Eventually::new(Always::new(Not::new(p1())))));
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), -1.184, epsilon = SIG_FIGS);
}

#[test]
fn case12() {
    let trace = load_test_trace();
    let formula = Always::new(Next::new(p1()));
    let distance = formula.distance(&trace);

    assert_eq!(distance.unwrap(), f64::NEG_INFINITY);
}

#[test]
fn case13() {
    let trace = load_test_trace();
    let formula = Eventually::new(Next::new(p1()));
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 3.7508, epsilon = SIG_FIGS);
}

#[test]
fn case14() {
    let trace = load_test_trace();
    let formula = Always::new(Next::new(Next::new(p1())));
    let distance = formula.distance(&trace);

    assert_eq!(distance.unwrap(), f64::NEG_INFINITY);
}

#[test]
fn case15() {
    let trace = load_test_trace();
    let formula = Next::new(Eventually::new(Next::new(p1())));
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 3.7508, epsilon = SIG_FIGS);
}

#[test]
fn case23() {
    let trace = load_test_trace();
    let formula = Not::new(Eventually::new_bounded((0.0, 3.5), Not::new(And::new(p2(), p1()))));
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 0.24923, epsilon = SIG_FIGS);
}

#[test]
fn case24() {
    let trace = load_test_trace();
    let formula = Not::new(Eventually::new_bounded((0.0, 1.0), Not::new(p1())));
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 2.0, epsilon = SIG_FIGS);
}

#[test]
fn case25() {
    let trace = load_test_trace();
    let formula = Eventually::new_bounded((0.1, 30.0), p1());
    let distance = formula.distance(&trace);

    assert_abs_diff_eq!(distance.unwrap(), 3.7508, epsilon = SIG_FIGS);
}