PRISM model checking (http://www.prismmodelchecker.org/manual/RunningPRISM/ModelChecking). The '-fixdl' switch is used, which means that all deadlock states in model are fixed by addition of self-loops.
source(new URL("http://bioputer.mimuw.edu.pl/tav4sb/workflows/setConstantCompactXmlList.bsh"));
input
output
org.embl.ebi.escience.scuflworkers.java.XMLInputSplitter
http://bioputer.mimuw.edu.pl/tav4sb/services/wsdl
prism
org.embl.ebi.escience.scuflworkers.java.XMLOutputSplitter
org.embl.ebi.escience.scuflworkers.java.StringListMerge
if (name != void) {
wrapped = "<results name=\""+name+"\">\n"+str+"\n</results>";
} else {
wrapped = "<results>\n"+str+"\n</results>";
}
str
name
wrapped
text/x-taverna-web-url
PRISM model file content.
Reference: http://www.prismmodelchecker.org/manual/ThePRISMLanguage/PRISMLanguageFiles
Example value:
// Enzymatic reaction model
ctmc
// Reaction rates constants
const double k1 = 0.184;
const double k2 = 0.016;
const double k3 = 0.211;
// Species s (Substrate)
const int s_MAX;
module s
s : [0..s_MAX] init s_MAX;
// r1 (ES-complex association)
[r1] s > 0 -> (s'=s-1);
// r2 (ES-complex dissociation)
[r2] s <= s_MAX-1 -> (s'=s+1);
endmodule
// Species e (Enzyme)
const int e_MAX;
module e
e : [0..e_MAX] init e_MAX;
// r1 (ES-complex association)
[r1] e > 0 -> (e'=e-1);
// r2 (ES-complex dissociation)
[r2] e <= e_MAX-1 -> (e'=e+1);
// r3 (Product creation)
[r3] e <= e_MAX-1 -> (e'=e+1);
endmodule
// Species es (ES-complex)
const int es_MAX = min(s_MAX, e_MAX);
module es
es : [0..es_MAX] init 0;
// r1 (ES-complex association)
[r1] es <= es_MAX-1 -> (es'=es+1);
// r2 (ES-complex dissociation)
[r2] es > 0 -> (es'=es-1);
// r3 (Product creation)
[r3] es > 0 -> (es'=es-1);
endmodule
// Species p (Product)
const int p_MAX = s_MAX;
module p
p : [0..p_MAX] init 0;
// r3 (Product creation)
[r3] p <= p_MAX-1 -> (p'=p+1);
endmodule
// Reaction rates
module reaction_rates
// r1 (ES-complex association)
[r1] (k1*s*e) > 0 -> (k1*s*e) : true;
// r2 (ES-complex dissociation)
[r2] (k2*es) > 0 -> (k2*es) : true;
// r3 (Product creation)
[r3] (k3*es) > 0 -> (k3*es) : true;
endmodule
// A expected number of enzyme-substrate complex association reactions.
rewards "r1"
[r1] true : 1;
endrewards
text/x-taverna-web-url
PRISM properties file content.
Reference:
http://www.prismmodelchecker.org/manual/PropertySpecification/PropertiesFiles
Example value:
// How many times on average a enzyme-substrate complex association reaction have to occure before the amount of product reaches 50% of it's maximum? Corresponds to EC50 coefficient.
// Attention: for this formula to make sense, the maximum amount of product must be known and set to the appropriate value; in this particular case it means that p_MAX must be equal to sum of initial amounts of all species, except of enzyme e.
R{"r1"}=? [ F (p >= 0.5 * p_MAX) ]
Optional constants and their values in the format of PRISM '-const' switch, i.e. comma separated definitons of constants: name=start:[step:]stop, where step is optional and by default equal to 1.
Reference:
http://www.prismmodelchecker.org/manual/RunningPRISM/Experiments
Example value:
e_MAX=1:2:15,s_MAX=1:10
A <results> XML element with list of results containing set of constants values and, for that set, a set of properties values or an error element with PRISM error message.
Example value:
<results>
<result>
<constant name="e_MAX">1</constant>
<constant name="s_MAX">1</constant>
<property name="R{"r1"}=? [ F (p>=0.5*p_MAX) ]">1.0758293745879832</property>
</result>
...
</results>