Extensible Promela Language Demo
This online demos will let you translate extended Promela
specifications down to pure Promela.
The extended Promela language used here extends Promela with three
language extensions:
- A non-deterministic choose construct that evaluates to a
random value in a specified range.
- A multi-dimensional array construct that allows one to
declare variables to be arrays of more than one dimension. Pure
Promela only provides direct support for single dimension arrays.
- A condition-table construct that is borrowed from
synchronous modelling languages like RSML or SCR.
Additional language extensions.
This extended Promela is constructed using the extensible language
tools developed by the MELT group. The distinguishing characteristic
of our approach to extensible langauges is that the language
extensions (like the three listed above) can be easily composed, even
if they are developed by different parties. You can read more about
our approach to extensible languages on our publications page.
Using the online demo
Select a demo specification from the drop-down menu below, or type
Promela code into the text box below, and then
click the "Compile" button. 
This will cause the code to be translated by our extended Promela
translator.
After it has
completed (it may take a few seconds), you will be taken to a page
that shows the original and translated (pure Promela) code or to a page that shows
errors detected in the submitted Promela code.
Additional language extensions
The extended version of Promela used in this demo incorporates 3
language extensions. We are working on other extensions that can be
used side-by-side with these three.
One of these is an extension for dimension and units of measurement
analysis.
We have implemented such an extension for our extensible specification
of ANSI C. There new types are added that specify if a value is
mearured in, for example, feet, centimeters, or
meters-per-second-squared. New type rules are added to ensure that
these values are not inappropritely used in assignment statements or
arithmetic operations. We will be implementing a version of this
extension for Promela as well soon.
Downloading the extensible Promela language framework We are
finalizing the Promela specification and will have it available for
download shortly. If you would like to obtain a "sneak-preview"
verion, please email Eric Van Wyk at evw@cs.umn.edu
|