#include "nuxmv.h"
#include <assert.h>
#include <stdio.h>
#include <stdlib.h>

/* === API usage for NuSMV example 'counter.smv' === */

const char *example_str = ""
                          "MODULE main\n"
                          "VAR\n"
                          "  bit0 : counter_cell(TRUE);\n"
                          "  bit1 : counter_cell(bit0.carry_out);\n"
                          "  bit2 : counter_cell(bit1.carry_out);\n"
                          "FAIRNESS TRUE;\n"
                          "LTLSPEC G F bit2.carry_out\n"
                          "\n"
                          "MODULE counter_cell(carry_in)\n"
                          "VAR\n"
                          "  value : boolean;\n"
                          "INIT value = FALSE;\n"
                          "TRANS next(value) = value xor carry_in;\n"
                          "DEFINE\n"
                          "  carry_out := value & carry_in;\n";

bool print_cb(char *chunk, size_t chunk_size, void *user_data)
{
    fwrite(chunk, 1, chunk_size, stdout);
    return true;
}

void print_symbol(nuxmv_env e, nuxmv_symbol s)
{
    if (nuxmv_symbol_is_scoped(e, s)) {
        print_symbol(e, nuxmv_symbol_get_scope(e, s));
        fputs(".", stdout);
    }
    fputs(nuxmv_symbol_get_name(e, s), stdout);
}

int main(int argc, const char **argv)
{
    /*** Create environment ***/
    nuxmv_env env = nuxmv_create_env();

    /*** Define types ***/
    nuxmv_expr_type bool_type = nuxmv_make_boolean_type(env);
    nuxmv_symbol false_sym = nuxmv_make_symbol(env, "FALSE");
    nuxmv_symbol true_sym = nuxmv_make_symbol(env, "TRUE");
    nuxmv_expr false_expr = nuxmv_make_value(env, false_sym, bool_type);
    nuxmv_expr true_expr = nuxmv_make_value(env, true_sym, bool_type);

    char buf[4096];
    bool ok;

    nuxmv_module main_module;
    nuxmv_model model;
    nuxmv_property prop;

    bool read_from_string = (argc > 1 && atoi(argv[1]));

    if (!read_from_string) {
        /*** Create counter_cell module ***/
        nuxmv_module counter_cell = nuxmv_create_module(env, "counter_cell");

        // Parameter: carry_in
        nuxmv_symbol carry_in_sym = nuxmv_make_symbol(env, "carry_in");
        nuxmv_expr carry_in_expr =
            nuxmv_make_identifier(env, carry_in_sym, bool_type);
        ok = nuxmv_module_add_params(env, counter_cell, &carry_in_expr, 1);
        assert(ok);

        // State variable: value
        nuxmv_symbol value_sym = nuxmv_make_symbol(env, "value");
        nuxmv_expr value_id = nuxmv_make_identifier(env, value_sym, bool_type);
        nuxmv_var_decl value_decl = {
            value_sym, nuxmv_make_simple_var_type(env, bool_type)};
        ok = nuxmv_module_add_state_var(env, counter_cell, value_decl);
        assert(ok);

        // INIT value = FALSE
        nuxmv_expr lhs = value_id;
        assert(NUXMV_VALID_EXPR(lhs));
        nuxmv_expr rhs = false_expr;
        nuxmv_expr eq = nuxmv_make_bin_op(env, NUXMV_OP_EQ, lhs, rhs);
        assert(NUXMV_VALID_EXPR(eq));
        ok = nuxmv_module_add_init(env, counter_cell, eq);
        assert(ok);

        // TRANS next(value) = value xor carry_in
        lhs = nuxmv_make_un_op(env, NUXMV_OP_NEXT_FUNCTION, value_id);
        rhs = nuxmv_make_bin_op(env, NUXMV_OP_XOR, value_id, carry_in_expr);
        assert(NUXMV_VALID_EXPR(rhs));
        eq = nuxmv_make_bin_op(env, NUXMV_OP_EQ, lhs, rhs);
        assert(NUXMV_VALID_EXPR(eq));
        ok = nuxmv_module_add_trans(env, counter_cell, eq);
        assert(ok);

        // DEFINE: carry_out := value & carry_in
        nuxmv_symbol carry_out_sym = nuxmv_make_symbol(env, "carry_out");
        nuxmv_expr carry_out_id =
            nuxmv_make_identifier(env, carry_out_sym, bool_type);
        nuxmv_expr carry_out_body =
            nuxmv_make_expr_from_string(env, "value & carry_in", counter_cell);
        assert(NUXMV_VALID_EXPR(carry_out_body));
        nuxmv_define_decl carry_out_define = {carry_out_id, carry_out_body};
        ok = nuxmv_module_add_define(env, counter_cell, carry_out_define);
        assert(ok);

        /*** Create main module ***/
        main_module = nuxmv_create_module(env, "main");
        assert(NUXMV_VALID_MODULE(main_module));

        // bit0 : counter_cell(TRUE)
        nuxmv_symbol bit0_symb = nuxmv_make_symbol(env, "bit0");
        ok = nuxmv_module_add_submodule(env, main_module,
                                        nuxmv_symbol_get_name(env, bit0_symb),
                                        counter_cell, &true_expr, 1);
        assert(ok);

        // bit1 : counter_cell(bit0.carry_out)
        nuxmv_symbol bit1_symb = nuxmv_make_symbol(env, "bit1");
        nuxmv_symbol bit0_carry_out_symb =
            nuxmv_make_scoped_symbol(env, "carry_out", bit0_symb);
        assert(NUXMV_VALID_SYMBOL(bit0_carry_out_symb));
        nuxmv_expr bit0_carry_out =
            nuxmv_make_identifier(env, bit0_carry_out_symb, bool_type);
        ok = nuxmv_module_add_submodule(env, main_module,
                                        nuxmv_symbol_get_name(env, bit1_symb),
                                        counter_cell, &bit0_carry_out, 1);
        assert(ok);

        // bit2 : counter_cell(bit1.carry_out)
        nuxmv_symbol bit2_symb = nuxmv_make_symbol(env, "bit2");
        nuxmv_symbol bit1_carry_out_symb =
            nuxmv_make_scoped_symbol(env, "carry_out", bit1_symb);
        nuxmv_expr bit1_carry_out =
            nuxmv_make_identifier(env, bit1_carry_out_symb, bool_type);
        ok = nuxmv_module_add_submodule(env, main_module,
                                        nuxmv_symbol_get_name(env, bit2_symb),
                                        counter_cell, &bit1_carry_out, 1);
        assert(ok);

        /*** Add property ***/
        // G F bit2.carry_out
        nuxmv_symbol bit2_carry_out_symb =
            nuxmv_make_scoped_symbol(env, "carry_out", bit2_symb);
        nuxmv_expr bit2_carry_out =
            nuxmv_make_identifier(env, bit2_carry_out_symb, bool_type);
        nuxmv_expr f_expr =
            nuxmv_make_un_op(env, NUXMV_OP_FINALLY, bit2_carry_out);
        assert(NUXMV_VALID_EXPR(f_expr));
        nuxmv_expr gf_expr = nuxmv_make_un_op(env, NUXMV_OP_GLOBALLY, f_expr);
        assert(NUXMV_VALID_EXPR(gf_expr));
        prop = nuxmv_make_property(env, NUXMV_PROPERTY_LTLSPEC, gf_expr,
                                   "carry_out_eventually");
        assert(NUXMV_VALID_PROPERTY(prop));
        ok = nuxmv_module_add_property(env, main_module, prop);
        assert(ok);

        printf("module hierarchy:\n");
        if (nuxmv_serialize_module_to_string(env, main_module, true, print_cb,
                                             NULL, buf, 4096) < 0) {
            printf("ERROR in serialization\n");
        }

        /*** Create and check model ***/
        model = nuxmv_create_model(env, main_module, NULL, 0);
        assert(NUXMV_VALID_MODEL(model));
    } else {
        model = nuxmv_create_model_from_string(env, NUXMV_MODEL_FORMAT_SMV,
                                               example_str);
        assert(NUXMV_VALID_MODEL(model));

        main_module = nuxmv_model_get_root_module(env, model);
        assert(NUXMV_VALID_MODULE(main_module));

        prop = nuxmv_model_get_property(env, model, 0);
        assert(NUXMV_VALID_PROPERTY(prop));
        assert(nuxmv_property_get_type(env, prop) == NUXMV_PROPERTY_LTLSPEC);
    }

    printf("\ninstantiated model:\n");
    if (nuxmv_serialize_model_to_string(env, model, NUXMV_MODEL_FORMAT_SMV,
                                        print_cb, NULL, buf, 4096) < 0) {
        printf("ERROR in serialization\n");
    }

    printf("\ntransition relation expressions:\n");
    for (int i = 0, n = nuxmv_model_get_trans_num(env, model); i < n; ++i) {
        nuxmv_expr trans = nuxmv_model_get_trans(env, model, i);
        assert(NUXMV_VALID_EXPR(trans));
        if (nuxmv_serialize_expr_to_string(env, trans, print_cb, NULL, buf,
                                           4096) < 0) {
            printf("ERROR in serialization\n");
        } else {
            printf("\n");
        }
    }

    nuxmv_opt myopts[100] = {{"algorithm", "rlive"},
                             {"max_bound", "10"},
                             {"force_smt", "false"},
                             {NULL, NULL}};
    int num_opts = 3;
    for (int i = 1; i + 1 < argc && i + 1 < 100; i += 2) {
        myopts[num_opts].key = argv[i];
        myopts[num_opts].value = argv[i + 1];
        ++num_opts;
    }

    nuxmv_result result =
        nuxmv_model_check_property(env, model, prop, myopts, num_opts);
    assert(NUXMV_VALID_RESULT(result));

    nuxmv_result_code rescode = nuxmv_result_get_code(env, result);
    assert(rescode != NUXMV_RESULT_INVALID);

    if (rescode == NUXMV_RESULT_TRUE) {
        printf("the property 'G F bit2.carry_out' is true\n");
    } else {
        assert(rescode == NUXMV_RESULT_UNKNOWN);
        printf("model checking returned unknown\n");
    }

    nuxmv_expr prop_expr =
        nuxmv_make_expr_from_string(env, "F G bit1.carry_out", main_module);
    assert(NUXMV_VALID_EXPR(prop_expr));
    prop = nuxmv_make_property(env, NUXMV_PROPERTY_LTLSPEC, prop_expr,
                               "bit1_carry_out_stabilizes");
    assert(NUXMV_VALID_PROPERTY(prop));

    result = nuxmv_model_check_property(env, model, prop, myopts, num_opts);
    assert(NUXMV_VALID_RESULT(result));

    rescode = nuxmv_result_get_code(env, result);
    assert(rescode != NUXMV_RESULT_INVALID);

    if (rescode == NUXMV_RESULT_FALSE) {
        printf("the property 'F G bit1.carry_out' is false. "
               "Here is a counterexample trace:\n");
        nuxmv_trace trace = nuxmv_result_get_trace(env, result);
        assert(NUXMV_VALID_TRACE(trace));
        int loop = nuxmv_trace_get_loopback(env, trace);
        assert(loop >= 0);
        printf("loopback at %d\n", loop);
        int sz = nuxmv_trace_get_step_num(env, trace);
        assert(sz > 0);
        for (int i = 0; i < sz; ++i) {
            printf("step [%d]\n", i);
            int n = nuxmv_trace_get_step_state_num(env, trace, i);
            assert(n >= 0);
            printf("state:\n");
            for (int j = 0; j < n; ++j) {
                nuxmv_trace_value v =
                    nuxmv_trace_get_step_state(env, trace, i, j);
                assert(NUXMV_VALID_TRACE_VALUE(v));
                nuxmv_expr var = v.identifier;
                nuxmv_expr val = v.value;
                ok = nuxmv_expr_is_identifier(env, var);
                assert(ok);
                ok = nuxmv_expr_is_value(env, val);
                assert(ok);
                fputs("  ", stdout);
                print_symbol(env, nuxmv_expr_get_symbol(env, var));
                printf(" := %s\n", nuxmv_symbol_get_name(
                                       env, nuxmv_expr_get_symbol(env, val)));
            }
            printf("inputs [%d -> %d]\n", i, i + 1 < sz ? i + 1 : loop);
            n = nuxmv_trace_get_step_input_num(env, trace, i);
            assert(n >= 0);

            for (int j = 0; j < n; ++j) {
                nuxmv_trace_value v =
                    nuxmv_trace_get_step_input(env, trace, i, j);
                assert(NUXMV_VALID_TRACE_VALUE(v));
                nuxmv_expr var = v.identifier;
                nuxmv_expr val = v.value;
                ok = nuxmv_expr_is_identifier(env, var);
                assert(ok);
                ok = nuxmv_expr_is_value(env, val);
                assert(ok);
                puts("  ");
                print_symbol(env, nuxmv_expr_get_symbol(env, var));
                printf(" := %s\n", nuxmv_symbol_get_name(
                                       env, nuxmv_expr_get_symbol(env, val)));
            }
        }
        printf("\ntrace in XML format:\n");
        if (nuxmv_serialize_trace_to_string(env, trace, NUXMV_TRACE_FORMAT_XML,
                                            print_cb, NULL, buf, 4096) < 0) {
            printf("ERROR in serialization\n");
        }
    } else {
        assert(rescode == NUXMV_RESULT_UNKNOWN);
        printf("model checking returned unknown\n");
    }

    ok = nuxmv_destroy_env(env);
    assert(ok);

    return 0;
}