:- use_module(library(plunit)).
% not necessary, except for separate compilation
:- use_module(reaction_rules).

:- begin_tests(revision, [condition(flag(slow_test, true, true)),
                          blocked(francois), setup((clear_model, reset_options))]).

test(
  'categorize_query',
  [
    true((ECTL, UCTL, ACTL) == (['EF'(a)], ['EU'(a, 'AG'(b))], ['AG'(b)]))
  ]
) :-
  revision:categorize_query(
    'EF'(a) /\ 'AG'(b) /\ 'EU'(a, 'AG'(b)),
    ECTL,
    UCTL,
    ACTL
  ).

test(
  'revise_model rule addition for ECTL',
  [
    setup(clear_model),
    all(Reactions = [[('MA'(1) for '_'=>b)],[('MA'(1) for a=>b)],[('MA'(1) for a=>b+a)]])
  ]
) :-
  command(present(a)),
  command(absent(b)),
  revision:revise_model('EU'(a, b), Reactions, []).

test(
  'revise_model rule addition for UCTL',
  [
    setup(clear_model),
    all(Reactions = [[('MA'(1)for a=>b)]])
  ]
) :-
  command(present(a)),
  command(absent(b)),
  revision:revise_model('EF'(b /\ 'AG'(not(a))), Reactions, []).

test(
  'revise_model rule deletion for ACTL, Miguel example',
  [
    setup(clear_model),
    all((Added, Removed) = [([], ['MA'(1) for a+b => b])])
  ]
) :-
  command(add_reaction(a => a + b)),
  command(add_reaction(a + b => b)),
  revision:revise_model(not(a) \/ 'AX'(a /\ b), Added, Removed).

test(
  'revise_model rule deletion (from counter-example) for ACTL',
  [
    setup(clear_model),
    all((Added, Removed) = [([],[('MA'(1)for a=>b)])])
  ]
) :-
  command(present(a)),
  command(absent(b)),
  command(add_reaction(a => b)),
  command(add_reaction(b => c)),
  revision:revise_model('AG'(a), Added, Removed).

test(
  'revise_model rule deletion for ACTL, Miguel bigger example',
  [
    setup(clear_model),
    all((Added, Removed) =
    [
      ([], [
        ('MA'(1)for'_'=>'_'),
        ('MA'(1)for'_'=>a),
        ('MA'(1)for a=>'_'),
        ('MA'(1)for a=>a),
        ('MA'(1)for a=>b),
        ('MA'(1)for b=>'_'),
        ('MA'(1)for b=>a),
        ('MA'(1)for a+b=>'_'),
        ('MA'(1)for b+a=>a),
        ('MA'(1)for a+b=>b)]
      )
    ])
  ]
) :-
  command(add_reaction('_' => '_')),
  command(add_reaction('_' => a)),
  command(add_reaction('_' => b)),
  command(add_reaction('_' => a+b)),
  command(add_reaction(a => '_')),
  command(add_reaction(a => a)),
  command(add_reaction(a => b)),
  command(add_reaction(a => a+b)),
  command(add_reaction(b => '_')),
  command(add_reaction(b => a)),
  command(add_reaction(b => b)),
  command(add_reaction(b => a+b)),
  command(add_reaction(a+b => '_')),
  command(add_reaction(a+b => a)),
  command(add_reaction(a+b => b)),
  command(add_reaction(a+b => a+b)),
  revision:revise_model(not(a) \/ 'AX'(a /\ b), Added, Removed).

test(
  '3_inhibitions',
  [
    setup(clear_model)
  ]
) :-
  command('_' => a),
  command('_' => b),
  command('_' => c),
  command(a => '_'),
  command(b => '_'),
  command(c => '_'),
  once(
    revision:revise_model(
      oscil(a) /\ oscil(b) /\ oscil(c) /\
      (c -> checkpoint(a, not(c))) /\
      (a -> checkpoint(b, not(a))) /\
      (b -> checkpoint(c, not(b))),
      Added,
      Removed
    )
  ),
  assertion(Added = ['MA'(1) for c+a=>a,'MA'(1) for a+b=>b,'MA'(1) for b+c=>c]),
  assertion(Removed = ['MA'(1) for a=>_,'MA'(1) for b=>_,'MA'(1) for c=>_]).

test(
  'Qu1',
  [
    setup(clear_model)
  ]
) :-
  command(load('library:examples/cell_cycle/Qu_et_al_2003.bc')),
  once(
    revision:revise_model(
      'AG'(not('CycB-CDK~{p1}') -> checkpoint('C25~{p1,p2}','CycB-CDK~{p1}')),
      Added,
      Removed
    )
  ),
  assertion(Added == []),
  assertion(Removed = [k1 for '_' => 'CycB']).


test(
  'Qu2',
  [
    setup(clear_model)
  ]
) :-
  command(load('library:examples/cell_cycle/Qu_et_al_2003.bc')),
  command(add_ctl(reachable('CycB'))),
  command(add_ctl(reachable('CycB-CDK~{p1}'))),
  command(add_ctl(reachable('CycB-CDK~{p1,p2}'))),
  command(add_ctl(reachable('APC'))),
  command(add_ctl(reachable('C25'))),
  command(add_ctl(reachable('C25~{p1}'))),
  command(add_ctl(oscil('C25~{p1,p2}'))),
  command(add_ctl(reachable('Wee1'))),
  command(add_ctl(reachable('Wee1~{p1}'))),
  command(add_ctl(reachable('CKI'))),
  command(add_ctl(reachable('CKI-CycB-CDK~{p1}'))),
  command(add_ctl(reachable('(CKI-CycB-CDK~{p1})~{p2}'))),
  command(add_ctl('AG'(not('APC')->checkpoint('CycB-CDK~{p1}','APC')))),
  command(add_ctl('AG'(not('C25~{p1,p2}')->checkpoint('C25~{p1}','C25~{p1,p2}')))),
  command(add_ctl('AG'(not('Wee1~{p1}')->checkpoint('Wee1','Wee1~{p1}')))),
  command(add_ctl('AG'(not('(CKI-CycB-CDK~{p1})~{p2}')->checkpoint('CKI-CycB-CDK~{p1}','(CKI-CycB-CDK~{p1})~{p2}')))),

  command(add_ctl('AG'(not('CycB-CDK~{p1}')->checkpoint('C25~{p1,p2}','CycB-CDK~{p1}')))),
  findall(Formula, item([kind: ctl_spec, item: Formula]), Specs),
  join_with_op(Specs, '/\\', Spec),
  once(
    revision:revise_model(
      Spec,
      Added,
      Removed
    )
  ),
  assertion(Added == []),
  assertion(Removed = [
    k5*['CycB-CDK~{p1,p2}']for'CycB-CDK~{p1,p2}'=>'CycB-CDK~{p1}',
    k15*['CKI-CycB-CDK~{p1}'] for 'CKI-CycB-CDK~{p1}'=>'CKI'+'CycB-CDK~{p1}'
  ]).


:- end_tests(revision).