<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> <html> <head> <title> PRISM Manual | ThePRISMLanguage / Introduction </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"> <meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska"> <link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon"> <link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon"> <!--HTMLHeader--><style type='text/css'><!-- ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; } code.escaped { white-space: nowrap; } .vspace { margin-top:1.33em; } .indent { margin-left:40px; } .outdent { margin-left:40px; text-indent:-40px; } a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; } a.createlink { text-decoration:none; position:relative; top:-0.5em; font-weight:bold; font-size:smaller; border-bottom:none; } img { border:0px; } .editconflict { color:green; font-style:italic; margin-top:1.33em; margin-bottom:1.33em; } table.markup { border:2px dotted #ccf; width:90%; } td.markup1, td.markup2 { padding-left:10px; padding-right:10px; } table.vert td.markup1 { border-bottom:1px solid #ccf; } table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; } table.markup caption { text-align:left; } div.faq p, div.faq pre { margin-left:2em; } div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; } div.faqtoc div.faq * { display:none; } div.faqtoc div.faq p.question { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; } div.faqtoc div.faq p.question * { display:inline; } .frame { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; } .lfloat { float:left; margin-right:0.5em; } .rfloat { float:right; margin-left:0.5em; } a.varlink { text-decoration:none; } .sourceblocklink { text-align: right; font-size: smaller; } .sourceblocktext { padding: 0.5em; border: 1px solid #808080; color: #000000; background-color: #f1f0ed; } .sourceblocktext div { font-family: monospace; font-size: small; line-height: 1; height: 1%; } .sourceblocktext div.head, .sourceblocktext div.foot { font: italic medium serif; padding: 0.5em; } --></style> <meta name='robots' content='index,follow' /> <link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css"> <link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css"> <link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css"> </head> <body text="#000000" bgcolor="#ffffff"> <div id="layout-maincontainer"> <div id="layout-main"> <div id="prism-mainbox"> <!-- ============================================================================= --> <!--PageHeaderFmt--> <!--/PageHeaderFmt--> <!--PageTitleFmt--> <div id="prism-man-title"> <p><a class='wikilink' href='Main.html'>The PRISM Language</a> / </p><h1>Introduction</h1> </div> <!--PageText--> <div id='wikitext'> <p>In order to construct and analyse a model with PRISM, it must be specified in the PRISM language, a simple, state-based language, based on the Reactive Modules formalism of Alur and Henzinger [<a class='wikilink' href='../Main/References.html#AH99'>AH99</a>]. This is used for all of the types of model that PRISM supports: discrete-time Markov chains (DTMCs), continuous-time Markov chains (CTMCs), Markov decision processes (MDPs) and probabilistic timed automata (PTAs). For background material on these models, look at the pointers to <a class='urllink' href='http://www.prismmodelchecker.org/about.php'>resources</a> on the PRISM web site. </p> <p class='vspace'>In this section, we describe the PRISM language and present a number of small illustrative examples. A precise definition of the semantics of the language is available from the "<a class='urllink' href='http://www.prismmodelchecker.org/doc/'>Documentation</a>" section of the PRISM web site. One of the best ways to learn what can be done with the PRISM language is to look at some existing examples. A number of these are included with the tool distribution in the <code>examples</code> directory. Many additional examples can be found on the "<a class='urllink' href='http://www.prismmodelchecker.org/casestudies/'>Case Studies</a>" section of the <a class='urllink' href='http://www.prismmodelchecker.org/'>PRISM website</a>. </p> <p class='vspace'>The fundamental components of the PRISM language are <em>modules</em> and <em>variables</em>. A model is composed of a number of <em>modules</em> which can interact with each other. A module contains a number of local <em>variables</em>. The values of these variables at any given time constitute the state of the module. The <em>global state</em> of the whole model is determined by the <em>local state</em> of all modules. The behaviour of each module is described by a set of <em>commands</em>. A command takes the form: </p> <div class='vspace'></div> <div class='sourceblock ' id='sourceblock1'> <div class='sourceblocktext'><div class="prism">[] <span class="prismident">guard</span> -> <span class="prismident">prob_1</span> : <span class="prismident">update_1</span> + ... + <span class="prismident">prob_n</span> : <span class="prismident">update_n</span>;<br/> </div></div> <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/ThePRISMLanguage/Introduction?action=sourceblock&num=1' type='text/plain'>[$[Get Code]]</a></div> </div> <p class='vspace'>The <em>guard</em> is a predicate over all the variables in the model (including those belonging to other modules). Each <em>update</em> describes a transition which the module can make if the guard is true. A transition is specified by giving the new values of the variables in the module, possibly as a function of other variables. Each update is also assigned a probability (or in some cases a rate) which will be assigned to the corresponding transition. </p> </div> <!--PageFooterFmt--> <div id='prism-man-footer'> </div> <!--/PageFooterFmt--> <!-- ============================================================================= --> </div> <!-- id="prism-mainbox" --> </div> <!-- id="layout-main" --> </div> <!-- id="layout-maincontainer" --> <div id="layout-leftcol"> <div id="prism-navbar2"> <h3><a class='wikilink' href='../Main/Main.html'>PRISM Manual</a></h3> <p><strong><a class='wikilink' href='Main.html'>The PRISM Language</a></strong> </p><ul><li><a class='selflink' href='Main.html'>Introduction</a> </li><li><a class='wikilink' href='Example1.html'>Example 1</a> </li><li><a class='wikilink' href='ModelType.html'>Model Type</a> </li><li><a class='wikilink' href='ModulesAndVariables.html'>Modules And Variables</a> </li><li><a class='wikilink' href='Commands.html'>Commands</a> </li><li><a class='wikilink' href='ParallelComposition.html'>Parallel Composition</a> </li><li><a class='wikilink' href='LocalNondeterminism.html'>Local Nondeterminism</a> </li><li><a class='wikilink' href='CTMCs.html'>CTMCs</a> </li><li><a class='wikilink' href='Example2.html'>Example 2</a> </li><li><a class='wikilink' href='Constants.html'>Constants</a> </li><li><a class='wikilink' href='Expressions.html'>Expressions</a> </li><li><a class='wikilink' href='Synchronisation.html'>Synchronisation</a> </li><li><a class='wikilink' href='ModuleRenaming.html'>Module Renaming</a> </li><li><a class='wikilink' href='MultipleInitialStates.html'>Multiple Initial States</a> </li><li><a class='wikilink' href='GlobalVariables.html'>Global Variables</a> </li><li><a class='wikilink' href='FormulasAndLabels.html'>Formulas And Labels</a> </li><li><a class='wikilink' href='PTAs.html'>PTAs</a> </li><li><a class='wikilink' href='CostsAndRewards.html'>Costs And Rewards</a> </li><li><a class='wikilink' href='ProcessAlgebraOperators.html'>Process Algebra Operators</a> </li><li><a class='wikilink' href='PRISMModelFiles.html'>PRISM Model Files</a> </li></ul><p>[ <a class='wikilink' href='AllOnOnePage.html'>View all</a> ] </p> </div> <!-- id="prism-navbar2" --> </div> <!-- id="layout-leftcol" --> </body> </html>