:- module(
  nusmv,
  [
    % options
    nusmv_initial_states/1,
    nusmv_counter_example/1,
    boolean_semantics/1,
    % commands
    export_nusmv/1,
    check_ctl/1,
    % API
    check_ctl_impl/5,
    enumerate_all_molecules/1
  ]
).

:- use_module(ctl).

% Only for separate compilation/linting
:- use_module(reaction_rules).


export_nusmv(OutputFile) :-
  biocham_command,
  type(OutputFile, output_file),
  doc('
    exports the current Biocham set of reactions and initial state in an SMV
    \\texttt{.smv} file.
  '),
  option(boolean_semantics, boolean_semantics, BoolSem,
    'Use positive or negative boolean semantics for inhibitors.'),
  export_nusmv_file(OutputFile, BoolSem).


export_nusmv_file(OutputFile, BoolSem) :-
  automatic_suffix(OutputFile, '.smv', write, FilenameSmv),
  setup_call_cleanup(
    open(FilenameSmv, write, Stream),
    export_nusmv_stream(Stream, BoolSem),
    close(Stream)
  ).


export_nusmv_stream(Stream, BoolSem) :-
  (
    is_reaction_model
  ->
    export_nusmv_stream_reactions(Stream)
  ;
    is_influence_model
  ->
    export_nusmv_stream_influences(Stream, BoolSem)
  ).


export_nusmv_stream_reactions(Stream) :-
  write(Stream, 'MODULE main\n\n'),
  findall(
    (Reactants, [], Products, []),
    (
      item([kind: reaction, item: Item]),
      reaction(Item, _, Reactants, Products)
    ),
    Reactions
  ),
  enumerate_all_molecules(Molecules),
  Molecules \= [],
  export_initial_state(Stream, Molecules),
  export_transitions(Stream, Molecules, Reactions).


enumerate_all_molecules(Molecules) :-
  (
    enumerate_molecules(ReactionMolecules)
  ->
    true
  ;
    ReactionMolecules = []
  ),
  (
    enumerate_molecules_influences(InfluenceMolecules)
  ->
    true
  ;
    InfluenceMolecules = []
  ),
  union(ReactionMolecules, InfluenceMolecules, ModelMolecules),
  (
    query_mols(QueryMolecules)
  ->
    true
  ;
    QueryMolecules = []
  ),
  union(ModelMolecules, QueryMolecules, Molecules).


export_initial_state(Stream, Molecules) :-
  forall(
    member(Molecule, Molecules),
    (
      make_nusmv_name(Molecule, Name),
      format(Stream, 'VAR ~a: boolean;\n', [Name]),
      get_initial_state(Molecule, InitialState),
      nusmv_initial_state(InitialState, NusmvInitialState),
      format(Stream, 'INIT ~a in ~a;~n', [Name, NusmvInitialState])
    )
  ),
  nl(Stream).


export_nusmv_stream_influences(Stream, BoolSem) :-
  write(Stream, 'MODULE main\n\n'),
  findall(
    (PositiveInputs, NegativeInputs, [Output | PositiveInputs], NegativeInputs),
    (
      item([kind: influence, item: Item]),
      influence(Item, _Force, PositiveInputs, NegInputs, '+', Output),
      (
        BoolSem == positive
      ->
        NegativeInputs = []
      ;
        subtract(NegInputs, [Output], NegativeInputs)
      )
    ),
    PInfluences
  ),
  findall(
    (PositiveInputs, NegativeInputs, PositiveInputs, [Output | NegativeInputs]),
    (
      item([kind: influence, item: Item]),
      influence(Item, __Force, PosInputs, NegInputs, '-', Output),
      (
        BoolSem == positive
      ->
        NegativeInputs = []
      ;
        NegativeInputs = NegInputs
      ),
      subtract(PosInputs, [Output], PositiveInputs)
    ),
    NInfluences
  ),
  append(PInfluences, NInfluences, Influences),
  enumerate_all_molecules(Molecules),
  export_initial_state(Stream, Molecules),
  export_transitions(Stream, Molecules, Influences).

:- dynamic(allmolecules/1).


export_transitions(Stream, Molecules, Reactions) :-
  retractall(allmolecules(_)),
  assertz(allmolecules(Molecules)),
  write(Stream, 'TRANS '),
  maplist(reaction_to_trans, Reactions, Trans),
  maplist(reaction_to_nofire, Reactions, Loops),
  all_nochange(NoChange),
  atomic_list_concat([NoChange | Loops], ' & ', Loop),
  atomic_list_concat([Loop | Trans], ' | ', TransOred),
  write(Stream, TransOred),
  nl(Stream).


reaction_to_trans((PositiveInputs, NegativeInputs, Products, Degraded), Trans) :-
  (
    PositiveInputs == []
  ->
    PositiveNames = [],
    NusmvPositive = 'TRUE'
  ;
    maplist(reactant_to_name, PositiveInputs, PositiveNames),
    apply_and_join(
      [make_nusmv_name],
      PositiveNames,
      ' & ',
      NusmvPositive
    )
  ),
  (
    NegativeInputs == []
  ->
    NegativeNames = [],
    NusmvNegative = 'TRUE'
  ;
    maplist(reactant_to_name, NegativeInputs, NegativeNames),
    apply_and_join(
      [make_nusmv_name, prepend_not],
      NegativeNames,
      ' & ',
      NusmvNegative
    )
  ),
  (
    Products == []
  ->
    ProductNames = [],
    NusmvProducts = 'TRUE'
  ;
    maplist(reactant_to_name, Products, ProductNames),
    apply_and_join(
      [make_nusmv_name, surround_next],
      ProductNames,
      ' & ',
      NusmvProducts
    )
  ),
  (
    Degraded == []
  ->
    DegradedNames = [],
    NusmvDegraded = 'TRUE'
  ;
    maplist(reactant_to_name, Degraded, DegradedNames),
    apply_and_join(
      [make_nusmv_name, surround_next, prepend_not],
      DegradedNames,
      ' & ',
      NusmvDegraded
    )
  ),
  allmolecules(Molecules),
  subtract(Molecules, PositiveNames, NoPositive),
  subtract(NoPositive, NegativeNames, NoNegative),
  subtract(NoNegative, ProductNames, NoProducts),
  subtract(NoProducts, DegradedNames, OtherMolecules),
  (
    OtherMolecules == []
  ->
    NusmvOthers = 'TRUE'
  ;
    apply_and_join(
      [make_nusmv_name, equiv_next],
      OtherMolecules,
      ' & ',
      NusmvOthers
    )
  ),
  atomic_list_concat(
    [NusmvPositive, NusmvNegative, NusmvProducts, NusmvDegraded, NusmvOthers],
    ' & ',
    Trans
  ).


reaction_to_nofire((PosInputs, NegInputs, _, _), ParenLoop) :-
  (
    PosInputs == []
  ->
    NusmvPos = 'FALSE'
  ;
    maplist(reactant_to_name, PosInputs, PosNames),
    apply_and_join(
      [make_nusmv_name, prepend_not],
      PosNames,
      ' | ',
      NusmvPos
    )
  ),
  (
    NegInputs == []
  ->
    NusmvNeg = 'FALSE'
  ;
    maplist(reactant_to_name, NegInputs, NegNames),
    apply_and_join(
      [make_nusmv_name],
      NegNames,
      ' | ',
      NusmvNeg
    )
  ),
  atomic_list_concat([NusmvPos, NusmvNeg], ' | ', Loop),
  format(atom(ParenLoop), '(~a)', [Loop]).


all_nochange(Result) :-
  allmolecules(Molecules),
  apply_and_join(
    [make_nusmv_name, equiv_next],
    Molecules,
    ' & ',
    Result
  ).


apply_and_join([], List, Join, Result) :-
  atomic_list_concat(List, Join, Result).

apply_and_join([Function | Functions], List, Join, Result) :-
  maplist(Function, List, NewList),
  apply_and_join(Functions, NewList, Join, Result).


surround_next(Atom, Next) :-
  format(atom(Next), 'next(~a)', [Atom]).


prepend_not(Atom, Not) :-
  format(atom(Not), '!~a', [Atom]).


equiv_next(Atom, Equiv) :-
  format(atom(Equiv), '(~a <-> next(~a))', [Atom, Atom]).


reactants_to_condition(Reactants, Condition) :-
  apply_and_join([reactant_to_name, make_nusmv_name], Reactants, ' & ', Condition).


reactant_to_name(_ * Name, Name) :-
  !.

reactant_to_name(Name, Name).


objects_to_condition(Objects, Condition) :-
  apply_and_join(make_nusmv_name, Objects, ' & ', Condition).


nusmv_initial_state(present(_), 'TRUE').

nusmv_initial_state(absent, 'FALSE').

nusmv_initial_state(undefined, '{FALSE, TRUE}').


make_nusmv_name(Molecule, Name) :-
  reserved(Molecule),
  !,
  atom_concat('_', Molecule, Name).


make_nusmv_name(Molecule, Name) :-
  atom_chars(Molecule, MoleculeChars),
  findall(
    TranslatedChar,
    (
      member(Char, MoleculeChars),
      (
        translate_char(Char, TranslatedChar)
      ->
        true
      ;
        TranslatedChar = Char
      )
    ),
    TranslatedList
  ),
  atomic_list_concat(TranslatedList, Name).


translate_char('_', '__').

translate_char(',', '_c').

translate_char('~', '').

translate_char('{', '_l').

translate_char('}', '_r').

translate_char('(', '_L').

translate_char(')', '_R').


reserved('B').

reserved('F').

reserved('G').

reserved('H').

reserved('O').

reserved('S').

reserved('T').

reserved('V').

reserved('W').

reserved('X').

reserved('Y').

reserved('Z').

reserved('A').

reserved('E').

reserved('U').

reserved('xor').

reserved('R').

reserved(Atom) :-
  ctl_unary_op(Atom).


ctl_unary_op(Op) :-
  memberchk(Op, ['AF', 'EF', 'AG', 'EG', 'AX', 'EX']).


:- grammar(boolean_semantics).

boolean_semantics(positive).

% Default. Set in library/initial.bc
boolean_semantics(negative).

:- grammar(nusmv_counter_example).

nusmv_counter_example(yes).

% Default. Set in library/initial.bc
nusmv_counter_example(no).

:- grammar(nusmv_initial_states).

nusmv_initial_states(some).

% Default. Set in library/initial.bc
nusmv_initial_states(all).


check_ctl(Query) :-
  biocham_command,
  doc('
    evaluates the \\argument{Query} on the current model by calling the
    NuSMV model-checker.

    As is usual in Model-Checking, the query is evaluated for all possible
    initial states (\\texttt{Ai} in Biocham v3). This can be changed via
    the \\texttt{nusmv_initial_states} option.
  '),
  type(Query, ctl),
  option(nusmv_initial_states, nusmv_initial_states, NusmvInitialState,
    'Consider that a query is true if verified for all/some initial states.'),
  option(nusmv_counter_example, nusmv_counter_example, NusmvCX,
    'Compute a counter-example for a query when possible.'),
  option(boolean_semantics, boolean_semantics, BoolSem,
    'Use positive or negative boolean semantics for inhibitors.'),
  check_ctl_impl(Query, NusmvInitialState, NusmvCX, BoolSem, Result),
  format('~w is ~w\n', [Query, Result]).


:- doc('\\begin{example}\n').
:- biocham_silent(clear_model).
:- biocham(present(a)).
:- biocham(absent(b)).
:- biocham(a => b).
:- biocham(a + b => a).
:- biocham(check_ctl('EX'(not(a) \/ 'EG'(not(b))), nusmv_counter_example:yes)).
:- biocham(check_ctl('EG'(not(b)), nusmv_counter_example:yes)).
:- biocham(check_ctl(reachable(b), nusmv_counter_example:yes)).
:- doc('\\end{example}').


check_ctl_impl(Query, some, NusmvCX, BoolSem, Result) :-
  check_ctl_impl(not(Query), all, NusmvCX, BoolSem, NotResult),
  (
    NotResult == 'true'
  ->
    Result = 'false'
  ;
    NotResult == 'false'
  ->
    Result = 'true'
  ;
    Result = 'error'
  ).


% stores the counter-example trace from NuSMV
% argument is a list, with R, then molecules in enumerate_all_molecules order
:- dynamic(trace/1).


% stores unknown molecules coming from the query
:- dynamic(query_mols/1).


% care that if Result is instantiated, the predicate might fail before parsing
% the full output/trace
check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :-
  retractall(trace(_)),
  retractall(query_mols(_)),
  normalize_query(Query, NQuery, Mols),
  assertz(query_mols(Mols)),
  translate_ctl_for_nusmv(NQuery, NusmvQuery),
  % FIXME better template, in $TMP, check if not existing, etc.
  export_nusmv_file(nusmv, BoolSem),
  open('nusmv.cmd', write, Stream),
  write(Stream, 'set input_file nusmv.smv\ngo\n'),
  (
    NusmvCX == 'no'
  ->
    write(Stream, 'set counter_examples 0\n')
  ;
    write(Stream, 'set default_trace_plugin 2\nset counter_examples 1\n')
  ),
  format(Stream, 'check_ctlspec -p "~a"\nquit\n', [NusmvQuery]),
  close(Stream),
  call_subprocess(
    path('NuSMV'),
    ['-df', '-source', 'nusmv.cmd'],
    [stdin(null), stdout(pipe(NusmvOut))]
  ),
  call_cleanup(parse_nusmv_out(NusmvOut, NusmvCX, Result), close(NusmvOut)),
  (
    NusmvCX == 'yes',
    trace(_)
  ->
    write('Trace:\n'),
    enumerate_all_molecules(Molecules),
    findall(T, trace(T), Trace),
    forall(
      member(Line, [Molecules | Trace]),
      (
        atomic_list_concat(Line, '\t', Atom),
        write(Atom),
        nl
      )
    ),
    nl
  ;
    true
  ).


translate_ctl_for_nusmv(A -> B, Atom) :-
  !,
  translate_ctl_for_nusmv(A, AA),
  translate_ctl_for_nusmv(B, BB),
  atomic_list_concat(['(', AA, ' -> ', BB, ')'], Atom).

translate_ctl_for_nusmv(A \/ B, Atom) :-
  !,
  translate_ctl_for_nusmv(A, AA),
  translate_ctl_for_nusmv(B, BB),
  atomic_list_concat(['(', AA, ' | ', BB, ')'], Atom).

translate_ctl_for_nusmv(A /\ B, Atom) :-
  !,
  translate_ctl_for_nusmv(A, AA),
  translate_ctl_for_nusmv(B, BB),
  atomic_list_concat(['(', AA, ' & ', BB, ')'], Atom).

translate_ctl_for_nusmv(not(A), Atom) :-
  !,
  translate_ctl_for_nusmv(A, AA),
  atomic_list_concat(['!', AA], Atom).

translate_ctl_for_nusmv('EU'(A, B), Atom) :-
  !,
  translate_ctl_for_nusmv(A, AA),
  translate_ctl_for_nusmv(B, BB),
  atomic_list_concat(['E [', AA, ' U ', BB, ']'], Atom).

translate_ctl_for_nusmv('AU'(A, B), Atom) :-
  !,
  translate_ctl_for_nusmv(A, AA),
  translate_ctl_for_nusmv(B, BB),
  atomic_list_concat(['A [', AA, ' U ', BB, ']'], Atom).

translate_ctl_for_nusmv(CTL, Atom) :-
  CTL =.. [Operator, A],
  ctl_unary_op(Operator),
  !,
  translate_ctl_for_nusmv(A, AA),
  atomic_list_concat([Operator, AA], ' ', Atom).

translate_ctl_for_nusmv(Object, Atom) :-
  make_nusmv_name(Object, Atom).


parse_nusmv_out(Out, NusmvCX, Result) :-
  read_line_to_codes(Out, Codes),
  (
    Codes = end_of_file
  ->
    Result = 'error'
  ;
    % "-- "
    Codes = [0'-, 0'-, 0'  | _]
  ->
    (
      append(_, [0'i, 0's, 0' , 0't, 0'r, 0'u, 0'e], Codes)
    ->
      Result = 'true'
    ;
      append(_, [0'i, 0's, 0' , 0'f, 0'a, 0'l, 0's, 0'e], Codes)
    ->
      Result = 'false'
    ;
      Result = 'error'
    ),
    (
      NusmvCX == 'no'
    ->
      true
    ;
      parse_nusmv_out_trace(Out)
    )
  ;
    parse_nusmv_out(Out, NusmvCX, Result)
  ).

parse_nusmv_out_trace(Out) :-
  % -- as demonstrated by the following execution sequence
  read_line_to_codes(Out, [0'-, 0'-, 0'  | _]),
  !,
  read_line_to_codes(Out, [0'N, 0'a, 0'm, 0'e, 0'\t | _]),
  read_string(Out, "\n", "\r", _End, InitialString),
  state_string_to_trace(InitialString, InitialTrace),
  assertz(trace(InitialTrace)),
  repeat,
  read_line_to_codes(Out, _Constants),
  read_line_to_codes(Out, _Inputs),
  read_string(Out, "\n", "\r", End, StateString),
  (
    End = -1
  ->
    !
  ;
    state_string_to_trace(StateString, StateTrace),
    assertz(trace(StateTrace)),
    fail
  ).

parse_nusmv_out_trace(Out) :-
  read_line_to_codes(Out, end_of_file).


state_string_to_trace(String, Trace) :-
  split_string(String, "\t", "\t", [_ | Trace]).


prolog:message(error(unknown_molecule)) -->
  ['Unknown molecule in query.'].