/* 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}
- <N,K1>.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
- <F>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").


