prism Web service

Created: 2011-01-26 21:53:24 Last updated: 2011-01-26 21:53:25

Download Workflow

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.

Preview

Download as scalable diagram (SVG)

Run

Run this Workflow in the Taverna Workbench...

Option 1:

Copy and paste this link into File > 'Open workflow location...'
http://myexperiment.org/workflows/1782/download?version=1
[ More Info Expand ]

Workflow Components

Inputs (3)

Name	Description
model	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] (k1se) > 0 -> (k1se) : true; // r2 (ES-complex dissociation) [r2] (k2es) > 0 -> (k2es) : true; // r3 (Product creation) [r3] (k3es) > 0 -> (k3es) : true; endmodule // A expected number of enzyme-substrate complex association reactions. rewards "r1" [r1] true : 1; endrewards
properties	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) ]
constants	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

Processors (6)

Name	Type	Description
setConstantCompactXmlList	beanshell
prismParamsCompactXML	local
prism	arbitrarywsdl
prismResultXML	local
Merge_string_list_to_string	local
wrapWithResultsTag	beanshell

Beanshells (2)

Name	Description	Inputs	Outputs
setConstantCompactXmlList		input	output
wrapWithResultsTag		str name	wrapped

Outputs (1)

Name	Description
resultsXml	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>

Links (9)

Source	Sink
constants	setConstantCompactXmlList:input
model	prismParamsCompactXML:model
properties	prismParamsCompactXML:properties
Merge_string_list_to_string:concatenated	wrapWithResultsTag:str
prism:prismResult	prismResultXML:input
prismParamsCompactXML:output	prism:prismParamsCompact
prismResultXML:result	Merge_string_list_to_string:stringlist
setConstantCompactXmlList:output	prismParamsCompactXML:constantCompact
wrapWithResultsTag:wrapped	resultsXml

Coordinations (0)

Information Workflow Type

Taverna 1

Information Uploader

trybik

Information License

All versions of this Workflow are licensed under:

Information Version 1 (of 1)

Information Credits (1)

(People/Groups)

trybik

Information Attributions (0)

(Workflows/Files)

None

Information Tags (5)

Uploader tags

Log in to add Tags

Information Shared with Groups (0)

None

Information Featured In Packs (0)

None

Log in to add to one of your Packs

Information Attributed By (0)

(Workflows/Files)

None

Information Favourited By (0)

No one

Information Statistics

1614 viewings

1347 downloads

[ see breakdown ]

Citations (0)

None

Version History

In chronological order:

prism Web service

Created by trybik on Wednesday 26 January 2011 21:53:24 (UTC)

Reviews (0)

No reviews yet

Be the first to review!

Comments (0)

View Timeline

No comments yet

Log in to make a comment

Other workflows that use similar services (10)

Only the first 2 workflows that use similar services are shown. View all workflows that use these services.

Taverna 1

Uploader

trybik

asynchronous prism Web service (1)

Download

Asynchronous version of the Prism Web service. Results XML list is sent via email.

Created: 2011-01-26 | Last updated: 2011-01-26

Credits: trybik

Taverna 1

Uploader

trybik

sbml2Prism Web service (1)

Download

For example of the SBML to PRISM translation and the description of its details see http://www.prismmodelchecker.org/manual/RunningPRISM/SupportForSBML .

Created: 2011-01-26 | Last updated: 2011-01-26

Credits: trybik