BioReSolve

A Prolog interpreter for Reaction Systems analysis

NEW! October 2022 Beta Release: slicingBioReSolve implements automatic, dynamic backward slicing driven by monitors!
Download the new slicing extension of BioReSolve (runs under SWI-Prolog)
NEW! March 2022 Beta Release: BioReSolvePlus can now handle delays, durations and concentration levels!
Download the new quantitative extension of BioReSolve (runs under SWI-Prolog)
Download the BioReSolve Prolog interpreter for Reaction Systems (runs under SWI-Prolog)
Download and edit the Reaction Systems specification template
See some instructions on how to use the BioReSolve tool.
Or just play online with a preliminary version of the tool: read how to use it.

Try it online (powered by Tau Prolog and Ace.js)

Main uncommented program (modify at your own risk):

MIT License

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NON INFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.

*/
:- use_module(library(lists)).

parse_ide(Str,Term) :- atom_chars(Str,Chars),phrase(ide(Term),Chars) .

ide(X) --> [C], { code_type(C, lower) } , ide_rest(Cs), { atom_chars(X, [C|Cs]) } .
ide_rest([]) --> [] .
ide_rest([C|Cs]) --> ide_next(C), ide_rest(Cs) .
ide_next(C) --> [C], { code_type(C, lower) } ;
                [C], { code_type(C, upper) } ;
                [C], { code_type(C, digit) } .
code_type('a',lower).
code_type('b',lower).
code_type('c',lower).
code_type('d',lower).
code_type('e',lower).
code_type('f',lower).
code_type('g',lower).
code_type('h',lower).
code_type('i',lower).
code_type('j',lower).
code_type('k',lower).
code_type('l',lower).
code_type('m',lower).
code_type('n',lower).
code_type('o',lower).
code_type('p',lower).
code_type('q',lower).
code_type('r',lower).
code_type('s',lower).
code_type('t',lower).
code_type('u',lower).
code_type('v',lower).
code_type('w',lower).
code_type('x',lower).
code_type('y',lower).
code_type('z',lower).
code_type('A',upper).
code_type('B',upper).
code_type('C',upper).
code_type('D',upper).
code_type('E',upper).
code_type('F',upper).
code_type('G',upper).
code_type('H',upper).
code_type('I',upper).
code_type('J',upper).
code_type('K',upper).
code_type('L',upper).
code_type('M',upper).
code_type('N',upper).
code_type('O',upper).
code_type('P',upper).
code_type('Q',upper).
code_type('R',upper).
code_type('S',upper).
code_type('T',upper).
code_type('U',upper).
code_type('V',upper).
code_type('W',upper).
code_type('X',upper).
code_type('Y',upper).
code_type('Z',upper).
code_type('0',digit).
code_type('1',digit).
code_type('2',digit).
code_type('3',digit).
code_type('4',digit).
code_type('5',digit).
code_type('6',digit).
code_type('7',digit).
code_type('8',digit).
code_type('9',digit).

parse_set(Str,Term) :- atom_chars(Str,Chars) , phrase(set_of_entities(Term),Chars) .

set_of_entities([]) --> ['{'] , blanks, ['}'] .
set_of_entities([E|Es]) --> ['{'] , blanks, ide(E) , blanks , set_of_entities_rest(Es) .
set_of_entities_rest([E|Es]) --> [','] , blanks, ide(E) , blanks , set_of_entities_rest(Es) .
set_of_entities_rest([]) --> ['}'] .
blanks --> [' '] , blanks , !.
blanks --> [].

parse_ctx(Str,Term) :- atom_chars(Str,Chars) , phrase(ctx_processes(Term),Chars) .

ctx_processes([]) --> ['['] , blanks , [']'] .
ctx_processes([K|Ks]) --> ['['] , blanks , ctx_process(K) , blanks , ctx_processes_rest(Ks) .
ctx_processes_rest([K|Ks]) --> [','] , blanks , ctx_process(K) , blanks , ctx_processes_rest(Ks) .
ctx_processes_rest([]) --> [']'] .

ctx_process(K) --> set_of_entities(C) , blanks , ['.'] , blanks , ctx_process(K1) , { K = pre(C,K1) } ;
                   ['('] , ctx_process(K1) , blanks , ctx_process_rest(Ks) , { summation([K1|Ks],K) } ;
                   ide(X) , { X == nil , K = nil } ;
                   ide(X) , { X \== nil, K = rec(X) } .
ctx_process_rest([K|Ks]) --> ['+'] , blanks, ctx_process(K) , blanks , ctx_process_rest(Ks) .
ctx_process_rest([]) --> [')'] .

summation([K],K) :- ! .
summation([K|Ks],plus(K,K1)) :- summation(Ks,K1) .

parse_env(Str,Term) :- atom_chars(Str,Chars) , phrase(env(Term),Chars) .

env([D|Ds]) --> ['['] , blanks , ide(X) , blanks , ['='] , blanks , ctx_process(K) , { D = def(X,K) } , blanks , env_rest(Ds) .
env_rest([D|Ds]) --> [','] , blanks , ide(X) , blanks , ['='] , blanks , ctx_process(K) , { D = def(X,K) } , blanks , env_rest(Ds) .
env_rest([]) --> [']'] .

parse_assert(Str,Term) :- atom_chars(Str,Chars) , phrase(formula_assert(Term),Chars) .

formula_assert(F) --> ['-'] , blanks , formula_assert(F1) , { F = not(F1) } ;
                      ['('] , blanks , formula_assert(F1) , blanks , ['^'] , blanks , formula_assert(F2) , blanks , [')'] , { F = xor(F1,F2) } ;
                      ['('] , blanks , formula_assert(F1) , blanks , formula_assert_rest_or(Fs) , { disjunction([F1|Fs],F) } ;
                      ['('] , blanks , formula_assert(F1) , blanks , formula_assert_rest_and(Fs) , { conjunction([F1|Fs],F) } ;
                      set_of_entities(C) , blanks , ['i','n','E'] , { F = sub(C,1) } ;
                      set_of_entities(C) , blanks , ['i','n','R'] , { F = sub(C,2) } ;
                      set_of_entities(C) , blanks , ['i','n','I'] , { F = sub(C,3) } ;
                      set_of_entities(C) , blanks , ['i','n','P'] , { F = sub(C,4) } ;
                      ['?'] , blanks , ['i','n','E'] , { F = nonempty(1) } ;
                      ['?'] , blanks , ['i','n','R'] , { F = nonempty(2) } ;
                      ['?'] , blanks , ['i','n','I'] , { F = nonempty(3) } ;
                      ['?'] , blanks , ['i','n','P'] , { F = nonempty(4) } .

formula_assert_rest_or([F|Fs]) --> ['*'] , blanks, formula_assert(F) , blanks , formula_assert_rest_or(Fs) .
formula_assert_rest_or([]) --> [')'] .
formula_assert_rest_and([F|Fs]) --> ['&'] , blanks, formula_assert(F) , blanks , formula_assert_rest_and(Fs) .
formula_assert_rest_and([]) --> [')'] .

disjunction([F],F) :- ! .
disjunction([F|Fs],or(F,F1)) :- disjunction(Fs,F1) .
conjunction([F],F) :- ! .
conjunction([F|Fs],and(F,F1)) :- conjunction(Fs,F1) .

parse_bhml(Str,Term) :- atom_chars(Str,Chars) , phrase(formula_bhml(Term),Chars) .

formula_bhml(G) --> ['t','r','u','e'] , { G=true } ;
                    ['f','a','l','s','e'] , { G=false } ;
                    ['('] , blanks , formula_bhml(G1) , blanks , formula_bhml_rest_or(Gs) , { disjunction([G1|Gs],G) } ;
                    ['('] , blanks , formula_bhml(G1) , blanks , formula_bhml_rest_and(Gs) , { conjunction([G1|Gs],G) } ;
                    ['<'] , blanks , formula_assert(F) , blanks , ['>'] , blanks ,formula_bhml(G1) , { G = diamond(F,G1) } ;
                    ['['] , blanks , formula_assert(F) , blanks , [']'] , blanks ,formula_bhml(G1) , { G = box(F,G1) } .

formula_bhml_rest_or([G|Gs]) --> ['*'] , blanks, formula_bhml(G) , blanks , formula_bhml_rest_or(Gs) .
formula_bhml_rest_or([]) --> [')'] .
formula_bhml_rest_and([G|Gs]) --> ['&'] , blanks, formula_bhml(G) , blanks , formula_bhml_rest_and(Gs) .
formula_bhml_rest_and([]) --> [')'] .

allIn([],_).
allIn([X|L1],L2):- member(X,L2), allIn(L1,L2).

both_lists([],_,[]).
both_lists([X|L1],L2,[X|L3]):- member(X,L2),!, both_lists(L1,L2,L3).
both_lists([_|L1],L2,L3):- both_lists(L1,L2,L3).
empty_inters(I,T):- both_lists(I,T,L), L=[].

non_empty(L):- length(L,N), N>=1.

enable(R,I,T):- allIn(R,T), empty_inters(I,T).

result(T,R,I,P,P):- enable(R,I,T),!.
result(_,_,_,_,[]).

union([],L,L).
union([X|L],L2,L3) :- member(X,L2), ! , union(L,L2,L3).
union([X|L],L2,[X|L3]) :- union(L,L2,L3).

find(_,[],[]).
find(X,[def(X,K)|_],K) :- !.
find(X,[def(_,_)|Ds],K) :- find(X,Ds,K).

unfold(_,nil,[]).
unfold(Delta,rec(X),Choices) :- find(X,Delta,K), unfold(Delta,K,Choices).
unfold(_,pre(C,K),[choice(C,[K])]).
unfold(Delta,plus(K1,K2),Choices) :- unfold(Delta,K1,Choices1),unfold(Delta,K2,Choices2),union(Choices1,Choices2,Choices).
unfold(_,[],[choice([],[])]).
unfold(Delta,[K|Ks],Choices) :- unfold(Delta,K,CK),unfold(Delta,Ks,CKs),shuffle(CK,CKs,Choices).

shuffle([],_,[]).
shuffle([choice(C,K)|CK],CKs,Choices) :- shuffle(choice(C,K),CKs,Ch1),
                                         shuffle(CK,CKs,Ch2),
                                         append(Ch1,Ch2,Choices).
shuffle(choice(_,_),[],[]).
shuffle(choice(C1,K1),[choice(C2,K2)|CKs],[choice(C,K)|Choices]) :- union(C1,C2,C),
                                                                    append(K1,K2,K),
                                                                    shuffle(choice(C1,K1),CKs,Choices).

oneTransition(sys(Delta,E,Ks,Rs),L,S) :- unfold(Delta,Ks,Choices),
                                         oneTransition(Delta,E,Choices,Rs,[tr(L,S)]).
oneTransition(Delta,E,[choice(C,K)|_],Rs,M) :- union(E,C,T),transition(Delta,T,K,Rs,M).
oneTransition(Delta,E,[_|Cs],Rs,M) :- oneTransition(Delta,E,Cs,Rs,M).

allTransitions(sys(Delta,E,Ks,Rs),Moves) :- unfold(Delta,Ks,Choices),
                                            allTransitions(Delta,E,Choices,Rs,Moves).
allTransitions(_,_,[],_,[]).
allTransitions(Delta,E,[choice(C,K)|Cs],Rs,Moves) :- union(E,C,T),transition(Delta,T,K,Rs,M),
                                                     allTransitions(Delta,E,Cs,Rs,Ms),
                                                     union(M,Ms,Moves).

transition(Delta,T,K,Rs,[tr(obs(T,R,RI,I,IR,P),sys(Delta,P,K,Rs))]) :- result(T,Rs,obs(T,R,RI,I,IR,P)).

result(T,[],obs(T,[],[],[],[],[])).
result(T,[react(R,I,P)|Rs],L) :- enable(R,I,T),!,result(T,Rs,L2),unionObs(obs(T,R,[],I,[],P),L2,L).
result(T,[react(R,I,_)|Rs],L) :- both_lists(I,T,RI),minusSet(R,T,IR),result(T,Rs,L2),unionObs(obs(T,[],RI,[],IR,[]),L2,L).

unionObs(obs(T,R1,RI1,I1,IR1,P1),obs(T,R2,RI2,I2,IR2,P2),obs(T,R,RI,I,IR,P)) :- union(R1,R2,R),
                                                                                union(RI1,RI2,RI),
                                                                                union(I1,I2,I),
                                                                                union(IR1,IR2,IR),
                                                                                union(P1,P2,P).

minusSet([],_,[]).
minusSet([X|R],T,Rs):- member(X,T),!,minusSet(R,T,Rs).
minusSet([X|R],T,[X|Rs]):- minusSet(R,T,Rs).

graph(S,Nodes,Arcs) :- graphAux([S],[],[],Nodes,Arcs).
graphAux([],Nodes,Arcs,Nodes,Arcs).
graphAux([S|Ss],Ns,As,Nodes,Arcs) :- member(S,Ns),!,
                                     graphAux(Ss,Ns,As,Nodes,Arcs).
graphAux([S|Ss],Ns,As,Nodes,Arcs) :- allTransitions(S,Moves),
                                     statesAndArcs(S,Moves,NewStates,NewArcs),
                                     append(NewStates,Ss,Ss1),
                                     union(NewArcs,As,As1),
                                     graphAux(Ss1,[S|Ns],As1,Nodes,Arcs).
statesAndArcs(_,[],[],[]).
statesAndArcs(S,[tr(L,S1)|Moves],NewStates,NewArcs) :- statesAndArcs(S,Moves,NewSs,NewAs),
                                                       union([S1],NewSs,NewStates),
                                                       union([arc(S,L,S1)],NewAs,NewArcs).
digraph(S,W) :- graph(S,Nodes,Arcs),
              atom_chars('digraph G {   node [shape=box]   edge [arrowhead = vee]   ',W1),
              nodes(Nodes,W2),
              edges(Arcs,W3),
              append([W1,W2,W3,['}']],W).

nodes([],[' ',' ',' ']).
nodes([sys(Delta,E,K,Rs)|Ns],W) :- writeNode(E,K,W1),nodes(Ns,W2),append([W1,[';',' ',' ',' '],W2],W).
edges([],[' ',' ',' ']).
edges([arc(sys(Delta,E,K,Rs),obs(T,R,RI,I,IR,P),sys(Delta,E1,K1,Rs1))|Ts],W) :- 
      writeNode(E,K,W1),writeNode(E1,K1,W2),atom_chars(' [ label = "',W3),writeE(T,W4),writeE(P,W5),edges(Ts,W6),
      append([W1,[' ','-','>',' '],W2,W3,W4,['>'],W5,['"',']',';',' ',' ',' '],W6],W).
writeNode([],K,W) :- !,writeKs(K,W1),append([['"','-'],W1,['"']],W).
writeNode(E,K,W) :- writeE(E,W1),writeKs(K,W2),append([['"'],W1,W2,['"']],W).
writeE([],[]).
writeE([A],W) :- atom_chars(A,W),!.
writeE([A|E],W) :- atom_chars(A,W1),writeE(E,W2),append([W1,[','],W2],W).
writeKs([],[]).
writeKs([K|Ks],W) :- writeK(K,W1),writeKs(Ks,W2),append([[' ','|',' '],W1,W2],W).
writeK(nil,['0']).
writeK(rec(X),W) :- atom_chars(X,W).
writeK(pre(C,K),W) :- writeE(C,W1),writeK(K,W2),append([W1,['.'],W2],W).
writeK(plus(K1,K2),W) :- writeK(K1,W1),writeK(K2,W2),append([W1,['+'],W2],W).

biosim(P,Q,F,BioRel) :- biosimRel([pair(P,Q)],[],F,BioRel).

biosimRel([],BR,_,BR).
biosimRel([pair(P,Q)|Rest],BR,F,BioRel) :- member(pair(P,Q),BR),
                                           biosimRel(Rest,BR,F,BioRel).
biosimRel([pair(P,Q)|Rest],BR,F,BioRel) :- \+ member(pair(P,Q),BR),
                                           P == Q,
                                           sim(P,Q,F,S1),
                                           append(Rest,S1,Rest1),
                                           biosimRel(Rest1,[pair(P,Q)|BR],F,BioRel).
biosimRel([pair(P,Q)|Rest],BR,F,BioRel) :- \+ member(pair(P,Q),BR),
                                           P \== Q,
                                           sim(P,Q,F,S1),
                                           sim(Q,P,F,S2),
                                           append(Rest,S1,Rest1),
                                           append(Rest1,S2,Rest2),
                                           biosimRel(Rest2,[pair(P,Q),pair(Q,P)|BR],F,BioRel).
sim(P,Q,F,S) :- allTransitionsF(F,P,Moves),
                checksim(Q,Moves,F,S).
checksim(_,[],_,[]).
checksim(Q,[tr(y,P1)|Ms],F,[pair(P1,Q1)|S]) :- oneTransition(Q,L,Q1),
                                               checkAssertion(L,F),
                                               checksim(Q,Ms,F,S).
checksim(Q,[tr(n,P1)|Ms],F,[pair(P1,Q1)|S]) :- oneTransition(Q,L,Q1),
                                               \+ checkAssertion(L,F),
                                               checksim(Q,Ms,F,S).

allTransitionsF(F,sys(Delta,E,Ks,Rs),Moves) :- unfold(Delta,Ks,Choices),
                                               allTransitionsF(F,Delta,E,Choices,Rs,Moves).
allTransitionsF(_,_,_,[],_,[]).
allTransitionsF(F,Delta,E,[choice(C,K)|Cs],Rs,Moves) :- union(E,C,T),transitionF(F,Delta,T,K,Rs,M),
                                                        allTransitionsF(F,Delta,E,Cs,Rs,Ms),
                                                        union(M,Ms,Moves).
transitionF(F,Delta,T,K,Rs,[tr(y,sys(Delta,P,K,Rs))]) :- result(T,Rs,obs(T,R,RI,I,IR,P)),checkAssertion(obs(T,R,RI,I,IR,P),F).
transitionF(F,Delta,T,K,Rs,[tr(n,sys(Delta,P,K,Rs))]) :- result(T,Rs,obs(T,R,RI,I,IR,P)),\+ checkAssertion(obs(T,R,RI,I,IR,P),F).

checkAssertion(_,true).
checkAssertion(L,sub(S,N)) :- select(N,L,X), allIn(S,X).
checkAssertion(L,nonempty(N)) :- select(N,L,X), non_empty(X).
checkAssertion(L,and(F1,F2)) :- checkAssertion(L,F1),checkAssertion(L,F2).
checkAssertion(L,or(F1,_)) :- checkAssertion(L,F1),!.
checkAssertion(L,or(_,F2)) :- checkAssertion(L,F2).
checkAssertion(L,xor(F1,F2)) :- checkAssertion(L,F1), \+ checkAssertion(L,F2).
checkAssertion(L,xor(F1,F2)) :- checkAssertion(L,F2), \+ checkAssertion(L,F1).
checkAssertion(L,not(F)) :- \+ checkAssertion(L,F).

select(1,obs(T,_,_,_,_,_),T).
select(2,obs(_,R,RI,_,_,_),U):-union(R,RI,U).
select(3,obs(_,_,_,I,IR,_),U):-union(I,IR,U).
select(4,obs(_,_,_,_,_,P),P).

checkBioHML(_,true,ok).
checkBioHML(S,false,no(S,false)).
checkBioHML(S,and(G1,_),B) :- checkBioHML(S,G1,B), B\==ok, !.
checkBioHML(S,and(_,G2),B) :- checkBioHML(S,G2,B), B\==ok, !.
checkBioHML(_,and(_,_),ok).
checkBioHML(S,or(G1,_),ok) :- checkBioHML(S,G1,ok),!.
checkBioHML(S,or(_,G2),ok) :- checkBioHML(S,G2,ok),!.
checkBioHML(S,or(G1,G2),no(S,[B1,B2])) :- checkBioHML(S,G1,B1),checkBioHML(S,G2,B2).
checkBioHML(S,diamond(F,G),B) :- allTransitions(S,Moves),filter(Moves,F,Ms),checkOne(S,F,Ms,G,B).
checkBioHML(S,box(F,G),B) :- allTransitions(S,Moves),filter(Moves,F,Ms),checkAll(S,Ms,G,B).

filter([],_,[]).
filter([tr(L,S)|Moves],F,[tr(L,S)|Ms]) :- checkAssertion(L,F),!,filter(Moves,F,Ms).
filter([tr(_,_)|Moves],F,Ms) :- filter(Moves,F,Ms).

checkOne(S,F,[],_,no(S,miss(F))).
checkOne(_,_,[tr(_,S1)|_],G,ok) :- checkBioHML(S1,G,ok),!.
checkOne(S,F,[tr(_,_)|Ms],G,B) :- checkOne(S,F,Ms,G,B).

checkAll(_,[],_,ok).
checkAll(S,[tr(L,S1)|_],G,no(S,has(L,B))) :- checkBioHML(S1,G,B), B\==ok, !.
checkAll(S,[tr(_,_)|Ms],G,B) :- checkAll(S,Ms,G,B).

main(digraph,Digraph) :- myenvironment(Delta),
                       myentities(E),
                       mycontext(Ks),
                       myreactions(Rs),
                       digraph(sys(Delta,E,Ks,Rs),W),
                       atom_chars(Digraph,W).

main(biohml,Answer) :- myenvironment(Delta),
                       myentities(E),
                       mycontext(Ks),
                       myreactions(Rs),
                       mybhml(G),
                       checkBioHML(sys(Delta,E,Ks,Rs),G,Answer).

main(biosim,BioRel) :- myenvironment(Delta),
                       myentities(E),
                       mycontext(Ks),
                       myreactions(Rs),
                       myassert(F),
                       advenvironment(Delta1),
                       adventities(E1),
                       advcontext(Ks1),
                       advreactions(Rs1),
                       biosim(sys(Delta,E,Ks,Rs),sys(Delta1,E1,Ks1,Rs1),F,BioRel).

main(adv,Digraph) :- advenvironment(Delta),
                     adventities(E),
                     advcontext(Ks),
                     advreactions(Rs),
                     digraph(sys(Delta,E,Ks,Rs),W),
                     atom_chars(Digraph,W).

Customizable clauses: (or you can just select one of the available examples below)
Examples: default, biosimilarity, lactose, heat-shock-response.

/* a Reaction System Process */ myenvironment([]). myentities([]). myreactions([react([a,b],[c],[b])]). mycontext(Ks) :- parse_ctx('[({a,b}.{a}.{a,c}.nil + {a,b}.{a}.{a}.nil)]',Ks). /* a BioHML formula to check */ mybhml(G) :- parse_bhml('<-{c} inE>[-{c} inE]<-{c} inE>true',G). /* a F-biosimilarity check against an adversary process */ myassert(F) :- parse_assert('-{c} inE',F). advenvironment([]). adventities([]). advreactions([react([a,b],[c],[b])]). advcontext(Ks) :- parse_ctx('[{a,b}.{a}.{a,c}.nil]',Ks).

Result:

Visualize the LTS in DOT format (Powered by Vis.js)

Authors
Linda Brodo Researcher in Computer Science Dipartimento di Scienze Economiche e Aziendali Università di Sassari Italy	Roberto Bruni Professor of Computer Science Dipartimento di Informatica Università di Pisa Italy	Moreno Falaschi Professor of Computer Science Dipartimento di Ingegneria dell'Informazione e Scienze Matematiche Università di Siena Italy

BioReSolve

A Prolog interpreter for Reaction Systems analysis

Try it online (powered by Tau Prolog and Ace.js)

Visualize the LTS in DOT format (Powered by Vis.js)

Authors