/* Template for Reaction System specifications A Reaction System is represented by a term of the form sys(Delta,E,Ks,Rs) where: - the "environment" Delta declares a set of process constant definitions - the set of "entities" E is the current (initial) state of the Reaction System - the "context" Ks is a list of context processes that provide some entities at each step - the set of "reactions" Rs defines the behaviour of the Reaction System The predicates main/2 and main/3 in the main file of the application refers to custom Reaction Systems, Assertions and BioHML formulas that can be set up by changing the predicates in this file. To experiment with a Reaction System you can rename and edit this file and then customize the application by changing the lines to import your definitions and set the working directory :- ["PATH/spec-FILE.pl"]. wdpath("PATH/"). where spec-FILE.pl is the name of the file and PATH is the actual path in your file system to spec-FILE.pl The predicates to be defined are: - myenvironment/1, mycontext/1, myentities/1, myreactions/1: custom Reaction System - myexperiment/2: a special kind of context - mybhml/1: a BioHML formula to check - myassert/1, advcontext/1, adventities/1, advreactions/1: for chcking bio-similarity of the custom Reaction System and an adversary Reaction System IMPORTANT: the custom and adversary Reaction Systems share the same environment Below you find the syntax to use for each specification and remember that: - entities and process constants can be any sequence of letters, _ and digits that starts with a small cap letter. */ /* myentities/1 and adventities/1 take a list of entities E. The list is not necessarily ordered and can contain repetitions, however it will be transformed in an ordered set before use */ myentities([a,b]). adventities([a]). % an adversary with a different set of initial entities /* myreactions/1 and advreactions/1 take a list of reactions. Each reaction is a term of the form react(R,I,P) where: - R is the list of reactants - I is the list of inhibitors - P is the list of products The lists R, I, P as well as the list of reactions are not necessarily ordered and can contain repetitions, however they will be transformed in ordered sets before use */ myreactions([react([a,b],[c],[b])]). advreactions(Rs) :- myreactions(Rs). % an adversary with the same reactions /* mycontext/1 takes a string-like description of a parallel composition of context processes The string will be converted to a proper term before use. A context-process K is either - nil: the null process - IDE: a constant identifier (it is important that the identifier is defined in the environment) - {C}.K: a context process K prefixed by a set of entities {C} - .K: a context process that makes N steps from context K1 and then behaves as context K - (K1 + ... + Kn): a nondeterministic choice between processes K1,...,Kn The parallel composition of context-processes is just a list of context processes. */ mycontext("[({a,b}.{a}.{a,c}.x + {a,b}.{a}.{a}.nil)]"). advcontext("[{a,b}.{a}.{a,c}.nil]"). % an adversary with a different context /* myenvironment/1 takes a string-like description of the environment The string will be converted to a proper term before use. An environment is a list of possibly recursive declarations of context-process constants Each declaration takes the form IDE = K */ myenvironment("[x = {a}.y, y =({a}.x + {b}.y)]"). /* myexperiment/2 is used to define a special kind of context for which several interesting analyses are possible. Such contexts have the form Q1. ... Q1.Q2. ... Q2.Q3. ... Q(n-1).Qn. ... Qn ... Additionally, the number Wi of occurrences of each Qi can be also specified. The general syntax is myexperiment([W1,W2, ... Wn],[Q1,Q2, ... Qn]). */ myexperiment([10,10],[[a,b],[a]]). /* myassert/1 takes a string-like description of a default assertion, e.g. for bio-simulation The string will be converted to a proper term before use. Assertions are predicates over the labels of the LTS An assertion F is either - ? inW: the non-emptyness test for the set of available entities - ? inR: the non-emptyness test for the set of meaningful reactants - ? inI: the non-emptyness test for the set of meaningful inhibitors - ? inP: the non-emptyness test for the set of products - C inW: the test for inclusion of C in the set of available entities - C inR: the test for inclusion of C in the set of meaningful reactants - C inI: the test for inclusion of C in the set of meaningful inhibitors - C inP: the test for inclusion of C in the set of products - -F: the negation of the assertion F - (F1 ^ F2): the xor of assertions F1 and F2 - (F1 \\/ ... \\/ Fn): the disjunction between assertions F1,...,Fn - (F1 /\\ ... /\\ Fn): the conjunction between assertions F1,...,Fn */ myassert("-{c} inW"). /* mybhml/1 takes a string-like description of a default BioHML formula The string will be converted to a proper term before use. A BioHML formula G is either - true - false - (G1 \\/ ... \\/ Gn): the disjunction between formulas G1,...,Gn - (G1 /\\ ... /\\ Gn): the conjunction between formulas G1,...,Gn - G: the diamond operator, where F is an assertion - [F]G: the box operator, where F is an assertion */ mybhml("<-{c} inW>[-{c} inW]<-{c} inW>true").