ctl.pl 10.4 KB
Newer Older
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
1 2 3 4 5 6
:- module(
  ctl,
  [
    % grammar
    ctl/1,
    % command
7 8 9 10
    add_ctl/1,
    delete_ctl/1,
    delete_ctl/0,
    list_ctl/0,
FAGES Francois's avatar
FAGES Francois committed
11 12
    generate_ctl/1,
    generate_ctl/0,
FAGES Francois's avatar
FAGES Francois committed
13
    generate_ctl_not/0,
FAGES Francois's avatar
FAGES Francois committed
14
    cleanup_ctl/0,
FAGES Francois's avatar
FAGES Francois committed
15
    expand_ctl/1,
16
    % API
17
    in_ctl/1,
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
18 19
    normalize_query/3
  ]
20
).
FAGES Francois's avatar
FAGES Francois committed
21

SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
22
% Only for separate compilation/linting
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
23 24
:- use_module(doc).
:- use_module(objects).
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
25
:- use_module(reaction_rules).
26

SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
27 28
:- use_module(nusmv). % for ctl_truth

FAGES Francois's avatar
FAGES Francois committed
29
:- doc('The Computation Tree Logic CTL can be used to express qualitative properties of the behavior of a network in a given (set of) initial states, at the boolean level of abstraction \\cite{CCDFS04tcs}.
FAGES Francois's avatar
FAGES Francois committed
30
CTL extends propositional logic with modal operators to specify where (E: on some path, A: on all paths)
FAGES Francois's avatar
FAGES Francois committed
31
and when (X: next state, F: finally at some future state, G: globally on all states, U: until a second formula is true, R: release)
FAGES Francois's avatar
FAGES Francois committed
32 33 34
a formula is true. As in any logic, these modalities can be combined with logical connectives and imbricated,
with the only restriction that a temporal operator must be immediately preceded by a path quantifier, 
e.g. \\texttt{EF(AG(p))} which expresses the reachability of a stable state where protein \\texttt{p} will always remain present.
35 36
CTL is well suited to analyze attractors, their reachability and transient properties  \\cite{TFFT16bi}.
It is worth noting however that CTL reachability properties are purely factual and not necessarily causal.').
FAGES Francois's avatar
FAGES Francois committed
37 38

:- doc('The syntax of CTL formulas and some useful abbreviations are defined by the following grammar:').
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
39 40 41

:- grammar(ctl).

FAGES Francois's avatar
FAGES Francois committed
42 43 44 45 46 47 48 49 50 51 52 53 54
ctl('EX'(E)) :-
  ctl(E).

ctl('EF'(E)) :-
  ctl(E).

ctl('EG'(E)) :-
  ctl(E).

ctl('EU'(E, F)) :-
  ctl(E),
  ctl(F).

FAGES Francois's avatar
FAGES Francois committed
55 56 57 58
ctl('ER'(E, F)) :-
  ctl(E),
  ctl(F).

FAGES Francois's avatar
FAGES Francois committed
59 60 61 62 63 64 65 66 67 68 69 70 71
ctl('AX'(E)) :-
  ctl(E).

ctl('AF'(E)) :-
  ctl(E).

ctl('AG'(E)) :-
  ctl(E).

ctl('AU'(E, F)) :-
  ctl(E),
  ctl(F).

FAGES Francois's avatar
FAGES Francois committed
72 73 74 75
ctl('AR'(E, F)) :-
  ctl(E),
  ctl(F).

76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
ctl(not(E)) :-
  ctl(E).

ctl(E /\ F) :-
  ctl(E),
  ctl(F).

ctl(E \/ F) :-
  ctl(E),
  ctl(F).

ctl(E -> F) :-
  ctl(E),
  ctl(F).

FAGES Francois's avatar
FAGES Francois committed
91 92 93 94
ctl(reachable(E)) :-
    ctl(E).
:- doc('\\emphright{reachable(f) is a shorthand for EF(f)}').

FAGES Francois's avatar
FAGES Francois committed
95
ctl(must_reach(E)) :-
FAGES Francois's avatar
FAGES Francois committed
96
    ctl(E).
FAGES Francois's avatar
FAGES Francois committed
97
:- doc('\\emphright{mustreach(f) is a shorthand for AF(f)}').
FAGES Francois's avatar
FAGES Francois committed
98 99 100 101 102 103 104 105 106 107 108 109

ctl(steady(E)) :-
  ctl(E).
:- doc('\\emphright{steady(f) is a shorthand for EG(f)}').

ctl(stable(E)) :-
  ctl(E).
:- doc('\\emphright{stable(f) is a shorthand for AG(f)}').

ctl(checkpoint(E, F)) :-
  ctl(E),
  ctl(F).
110
:- doc('\\emphright{checkpoint(f, g) is a shorthand for not EU(not f, g)). Note that such a factual property does not imply any causality relationship from f to g.}').
FAGES Francois's avatar
FAGES Francois committed
111

FAGES Francois's avatar
FAGES Francois committed
112 113 114
ctl(checkpoint2(E, F)) :-
  ctl(E),
  ctl(F).
115 116
%:- doc('\\emphright{checkpoint2(f, g) is a shorthand for EF(not f)/\\\\EF(g)/\\\\checkpoint(f,g)}'). % good point for EF(g) not sure for EF(not f)
:- doc('\\emphright{checkpoint2(f, g) is a shorthand for EF(g)/\\\\checkpoint(f,g)}'). 
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
117

FAGES Francois's avatar
FAGES Francois committed
118 119 120 121
%ctl(predecessor_checkpoint(E, F)) :-
%  ctl(E),
%  ctl(F).
%:- doc('\\emphright{predecessor_checkpoint(f, g) is a shorthand for AG(not g -> checkpoint(f, g)) which is true if the non trivial reachability of g, if any, is always preceded by a sequence of f}').
FAGES Francois's avatar
FAGES Francois committed
122

FAGES Francois's avatar
FAGES Francois committed
123
ctl(oscil2(E)) :-
FAGES Francois's avatar
FAGES Francois committed
124
  ctl(E).
FAGES Francois's avatar
FAGES Francois committed
125
:- doc('\\emphright{oscil2(f) is a shorthand for EU(not(f), f /\\\\ EU(f, not(f) /\\\\ EU(not(f), f))) which is true if f has at least two peaks on one path}').
FAGES Francois's avatar
FAGES Francois committed
126

FAGES Francois's avatar
FAGES Francois committed
127
ctl(oscil3(E)) :-
FAGES Francois's avatar
FAGES Francois committed
128
  ctl(E).
FAGES Francois's avatar
FAGES Francois committed
129 130 131 132 133 134
:- doc('\\emphright{oscil3(f) is a shorthand for EU(not(f), f /\\\\ EU(f, not(f) /\\\\ EU(not(f), f /\\\\ EU(f, not(f) /\\\\ EU(not(f), f))))) which is true if f has at least three peaks on one path}').

ctl(oscil(E)) :-
  ctl(E).
:- doc('\\emphright{oscil(f) is a shorthand for  oscil3(f) /\\\\ EG(EF(f) /\\\\ EF(not f)) which is a necessary (not sufficient) condition for infinite oscillations in CTL}').

FAGES Francois's avatar
FAGES Francois committed
135

SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
136

137
ctl(current_spec).
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
138 139

ctl(E) :-
FAGES Francois's avatar
FAGES Francois committed
140
    object(E).
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
141

142 143


144 145


FAGES Francois's avatar
FAGES Francois committed
146 147
:- devdoc('\\section{Commands}').

FAGES Francois's avatar
FAGES Francois committed
148
:- doc('The qualitative behavior of a network can be specified by a set of CTL formulas using the following commands:').
FAGES Francois's avatar
FAGES Francois committed
149 150 151 152 153 154 155


list_ctl :-
  biocham_command,
  doc('Prints out all formulae from the current CTL specification.'),
  % model: current_model?
  list_items([kind: ctl_spec]).
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
156

FAGES Francois's avatar
FAGES Francois committed
157
expand_ctl(Formula) :-
FAGES Francois's avatar
FAGES Francois committed
158 159 160 161 162 163
  biocham_command,
  type(Formula, ctl),
  doc('shows the expansion in CTL of a formula with patterns.'),
  normalize_query(Formula,ExpandedFormula,_),
  format('~w\n', [ExpandedFormula]).

164 165 166 167
add_ctl(Formula) :-
  biocham_command,
  type(Formula, ctl),
  doc('Adds a CTL formula to the currently declared CTL specification.'),
FAGES Francois's avatar
FAGES Francois committed
168
  (in_ctl(Formula) -> true ; add_item([kind: ctl_spec, item: Formula])).
169 170 171 172 173 174 175 176 177 178


delete_ctl(Formula) :-
  biocham_command,
  type(Formula, ctl),
  doc('Removes a CTL formula to the currently declared CTL specification.'),
  find_item([id: Id, type: ctl_spec, item: Formula]),
  delete_item(Id).


179
in_ctl(Formula) :-
FAGES Francois's avatar
FAGES Francois committed
180
    devdoc('checks whether a formula belongs to the current CTL specification, syntactically.'),
181 182 183
    item([type: ctl_spec, item: Formula]).


184 185 186 187 188 189
delete_ctl :-
  biocham_command,
  doc('Removes all formulae from the current CTL specification.'),
  % model: current_model?
  delete_items([kind: ctl_spec]).

FAGES Francois's avatar
FAGES Francois committed
190
:- doc('The set of CTL formulas of some simple form that are true in the current set of initial states
FAGES Francois's avatar
FAGES Francois committed
191
can also be automatically generated as a specification of the network using the following commands.').
192

FAGES Francois's avatar
FAGES Francois committed
193 194 195
:- devdoc('\\begin{todo} generate_ctl options on:{molecules} between:{molecules}\\end{todo}').


FAGES Francois's avatar
FAGES Francois committed
196
generate_ctl(Formula):-
197
  biocham_command,
FAGES Francois's avatar
FAGES Francois committed
198
  type(Formula, ctl),
FAGES Francois's avatar
FAGES Francois committed
199
  doc('adds to the CTL specification all the CTL formulas that are true, not subsumed by another CTL formula in the specification, and that match the argument formula in which the names that are not molecules are treated as wildcards and replaced by distinct molecules of the network. This command is a variant with subsumption test of \\command{add_ctl} if all names match network molecule names, otherwise it enumerates all m^v instances (where m is the number of molecules and v the number of wildcards in the formula).'),
FAGES Francois's avatar
FAGES Francois committed
200 201
  normalize_query(Formula,F,Leaves),
  enumerate_molecules(Molecules),
202 203 204 205 206
  subtract(Leaves,Molecules,L),
  length(L,N),
  length(Wildcards,N),
  substitute(L,Wildcards,F,S),
  substitute(L,Wildcards,Formula,Spec), % for pretty spec
FAGES Francois's avatar
FAGES Francois committed
207 208
  \+ (
      enumerate_instances(Wildcards,Molecules),
209 210
      \+ cleanup_ctl(S),
      \+ cleanup_ctl(Spec),
FAGES Francois's avatar
FAGES Francois committed
211
      ctl_truth(S, true),
FAGES Francois's avatar
FAGES Francois committed
212
      print(Spec),nl,
FAGES Francois's avatar
FAGES Francois committed
213
      \+ add_ctl(Spec)
214 215 216
  ).

    
FAGES Francois's avatar
FAGES Francois committed
217 218
generate_ctl:-
  biocham_command,
219
  doc('adds to the CTL specification all reachable stable, reachable steady, reachable, checkpoint2, and oscil formulas on all molecules (using this order of enumeration for performing subsumption checks).'),
FAGES Francois's avatar
FAGES Francois committed
220
  generate_ctl(reachable(stable(wildcard))),
221 222
  generate_ctl(reachable(steady(wildcard))),
  generate_ctl(reachable(wildcard)),
FAGES Francois's avatar
FAGES Francois committed
223
  generate_ctl(checkpoint2(wildcard,dummy)),
FAGES Francois's avatar
FAGES Francois committed
224 225 226
  generate_ctl(oscil(wildcard)),
  generate_ctl(oscil3(wildcard)),
  generate_ctl(oscil2(wildcard)). 
FAGES Francois's avatar
FAGES Francois committed
227 228 229 230 231



generate_ctl_not:-
  biocham_command,
232
  doc('adds to the CTL specification all reachable stable , reachable stable not, reachable steady, reachable steady not, reachable, reachable not, checkpoint2, and oscil formulas on all molecules.'),
FAGES Francois's avatar
FAGES Francois committed
233 234
  generate_ctl(reachable(stable(wildcard))),
  generate_ctl(reachable(stable(not(wildcard)))),
235 236 237 238
  generate_ctl(reachable(steady(wildcard))),
  generate_ctl(reachable(steady(not(wildcard)))),
  generate_ctl(reachable(wildcard)),
  generate_ctl(reachable(not(wildcard))),
FAGES Francois's avatar
FAGES Francois committed
239 240
  generate_ctl(checkpoint2(wildcard,dummy)),
  generate_ctl(checkpoint2(wildcard,not(dummy))), 
FAGES Francois's avatar
FAGES Francois committed
241 242
  generate_ctl(checkpoint2(not(wildcard),dummy)),
  generate_ctl(checkpoint2(not(wildcard),not(dummy))), 
FAGES Francois's avatar
FAGES Francois committed
243 244 245
  generate_ctl(oscil(wildcard)),
  generate_ctl(oscil3(wildcard)),
  generate_ctl(oscil2(wildcard)). 
FAGES Francois's avatar
FAGES Francois committed
246 247


248 249 250 251 252
cleanup_ctl:-
    biocham_command,
    doc('cleans up the CTL specification by removing redundant formulae such as reachable(steady(A)) if reachable(stable(A)) is true, etc.'),
    devdoc('This command will be generalized when the CTL abbreviations will be functions.'),
    \+ (
253
      item([kind: ctl_spec, id: Id, item: Formula]),
254
      cleanup_ctl(Formula),
255
      \+ delete_item(Id)
256 257 258 259 260 261 262 263 264 265 266
    ),
    list_ctl.

cleanup_ctl(reachable(steady(A))):-
    !,
    in_ctl(reachable(stable(A))).

cleanup_ctl(reachable(A)):-
    !,
    (in_ctl(reachable(steady(A)));
     in_ctl(reachable(stable(A)));
FAGES Francois's avatar
FAGES Francois committed
267 268
     in_ctl(oscil(A));in_ctl(oscil2(A));in_ctl(oscil3(A));
     (A=not(B), (in_ctl(oscil(B));in_ctl(oscil2(B));in_ctl(oscil3(B))))
269 270
    ),
    !.
271

FAGES Francois's avatar
FAGES Francois committed
272 273 274 275 276
cleanup_ctl(oscil2(A)):-
    !,
    in_ctl(oscil(A));in_ctl(oscil3(A)).

cleanup_ctl(oscil3(A)):-
277 278 279 280 281
    !,
    in_ctl(oscil(A)).



FAGES Francois's avatar
FAGES Francois committed
282

283 284 285 286 287 288 289
:- doc('\\begin{example}').
:- biocham_silent(clear_model).
:- biocham(a=>b).
:- biocham(b=>c).
:- biocham(c=>d).
:- biocham(present(b)).
:- biocham(make_absent_not_present).
FAGES Francois's avatar
FAGES Francois committed
290
:- biocham(generate_ctl(checkpoint2(x,d))).
FAGES Francois's avatar
FAGES Francois committed
291
:- biocham(generate_ctl_not).
292
:- doc('\\end{example}').
FAGES Francois's avatar
FAGES Francois committed
293

FAGES Francois's avatar
FAGES Francois committed
294 295 296



FAGES Francois's avatar
FAGES Francois committed
297 298 299 300 301 302 303 304 305 306 307 308
:- devdoc('\\section{API predicates}').


:-devdoc('\\section{Internal predicates}').

enumerate_instances([V|Variables],Molecules):-
    select(V,Molecules,Molecules2),
    enumerate_instances(Variables,Molecules2).

enumerate_instances([],_).

:- devdoc('Internal predicates.').
309 310


SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
311 312 313 314 315 316 317 318 319
normalize_query(Query, NQuery, SLeaves) :-
  normalize_query(Query, NQuery, [], Leaves),
  sort(Leaves, SLeaves).


normalize_query(reachable(Q), QQ, L1, L2) :-
  !,
  normalize_query('EF'(Q), QQ, L1, L2).

FAGES Francois's avatar
FAGES Francois committed
320 321 322 323
normalize_query(must_reach(Q), QQ, L1, L2) :-
  !,
  normalize_query('AF'(Q), QQ, L1, L2).

FAGES Francois's avatar
FAGES Francois committed
324 325 326 327 328 329 330 331
normalize_query(steady(Q), QQ, L1, L2) :-
  !,
  normalize_query('EG'(Q), QQ, L1, L2).

normalize_query(stable(Q), QQ, L1, L2) :-
  !,
  normalize_query('AG'(Q), QQ, L1, L2).

SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
332 333
normalize_query(oscil(Q), QQ, L1, L2) :-
  !,
FAGES Francois's avatar
FAGES Francois committed
334
  normalize_query(oscil3(Q) /\ 'EG'('EF'(Q) /\ 'EF'(not(Q))), QQ, L1, L2).
SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
335

FAGES Francois's avatar
FAGES Francois committed
336
normalize_query(oscil2(Q), QQ, L1, L2) :-
FAGES Francois's avatar
FAGES Francois committed
337
  !,
FAGES Francois's avatar
FAGES Francois committed
338
  normalize_query('EU'(not(Q), Q /\ 'EU'(Q, not(Q) /\ 'EU'(not(Q), Q))), QQ, L1, L2).
FAGES Francois's avatar
FAGES Francois committed
339

FAGES Francois's avatar
FAGES Francois committed
340 341 342
normalize_query(oscil3(Q), QQ, L1, L2) :-
  !,
  normalize_query('EU'(not(Q), Q /\ 'EU'(Q, not(Q) /\ 'EU'(not(Q), Q /\ 'EU'(Q, not(Q) /\ 'EU'(not(Q), Q))))), QQ, L1, L2).
FAGES Francois's avatar
FAGES Francois committed
343

SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
344 345 346 347
normalize_query(checkpoint(A, B), QQ, L1, L2) :-
  !,
  normalize_query(not('EU'(not(A), B)), QQ, L1, L2).

FAGES Francois's avatar
FAGES Francois committed
348 349
normalize_query(checkpoint2(A, B), QQ, L1, L2) :-
  !,
FAGES Francois's avatar
FAGES Francois committed
350
  normalize_query('EF'(B) /\ not('EU'(not(A), B)), QQ, L1, L2).
FAGES Francois's avatar
FAGES Francois committed
351

FAGES Francois's avatar
FAGES Francois committed
352 353 354
%normalize_query(predecessor_checkpoint(A, B), QQ, L1, L2) :-
%  !,
%  normalize_query('AG'(not(B) -> checkpoint(A,B)), QQ, L1, L2).
FAGES Francois's avatar
FAGES Francois committed
355

SOLIMAN Sylvain's avatar
SOLIMAN Sylvain committed
356 357 358 359 360 361 362 363 364
normalize_query(Q, Q, L, [Q | L]) :-
  atomic(Q),
  !.

normalize_query(Q, QQ, L1, L2) :-
  Q =.. [Functor | Args],
  % maplist(normalize_query, Args, QArgs),
  foldl(normalize_query, Args, QArgs, L1, L2),
  QQ =.. [Functor | QArgs].