Browse Source
Moved PEPA-to-PRISM source code from main distribution to separate area.
Moved PEPA-to-PRISM source code from main distribution to separate area.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@503 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
19 years ago
56 changed files with 0 additions and 3521 deletions
-
13prism/src/pepa/src/Alphabets.sig
-
54prism/src/pepa/src/Alphabets.sml
-
341prism/src/pepa/src/COPYING
-
10prism/src/pepa/src/CommandLine.sig
-
15prism/src/pepa/src/CommandLine.sml
-
18prism/src/pepa/src/Debugging.sig
-
39prism/src/pepa/src/Debugging.sml
-
12prism/src/pepa/src/Derivatives.sig
-
47prism/src/pepa/src/Derivatives.sml
-
22prism/src/pepa/src/Error.sig
-
54prism/src/pepa/src/Error.sml
-
11prism/src/pepa/src/Extractor.sig
-
35prism/src/pepa/src/Extractor.sml
-
17prism/src/pepa/src/Files.sig
-
41prism/src/pepa/src/Files.sml
-
5prism/src/pepa/src/JAVA/Makefile
-
10prism/src/pepa/src/JAVA/pepa/compiler/InternalError.java
-
60prism/src/pepa/src/JAVA/pepa/compiler/Main.java
-
18prism/src/pepa/src/Lexer.sig
-
46prism/src/pepa/src/Lexer.sml
-
14prism/src/pepa/src/Lists.sig
-
28prism/src/pepa/src/Lists.sml
-
13prism/src/pepa/src/Makefile
-
71prism/src/pepa/src/Makefile.mosml
-
15prism/src/pepa/src/PEPA2PRISM.sig
-
771prism/src/pepa/src/PEPA2PRISM.sml
-
10prism/src/pepa/src/Parser.sig
-
183prism/src/pepa/src/Parser.sml
-
33prism/src/pepa/src/Pepa.sig
-
54prism/src/pepa/src/Pepa.sml
-
12prism/src/pepa/src/Prettyprinter.sig
-
88prism/src/pepa/src/Prettyprinter.sml
-
59prism/src/pepa/src/README
-
22prism/src/pepa/src/README.TOO
-
12prism/src/pepa/src/Semantic.sig
-
154prism/src/pepa/src/Semantic.sml
-
11prism/src/pepa/src/Sort.sig
-
24prism/src/pepa/src/Sort.sml
-
8prism/src/pepa/src/TESTS/ERRORS/README
-
7prism/src/pepa/src/TESTS/ERRORS/activeactive.pepa
-
4prism/src/pepa/src/TESTS/ERRORS/ratemissing.pepa
-
7prism/src/pepa/src/TESTS/README
-
110prism/src/pepa/src/TESTS/auction.pepa
-
288prism/src/pepa/src/TESTS/auction_pepa.sm
-
22prism/src/pepa/src/TESTS/badge.1.4.pepa
-
121prism/src/pepa/src/TESTS/badge.1.4_pepa.sm
-
6prism/src/pepa/src/TESTS/hiding.pepa
-
44prism/src/pepa/src/TESTS/hiding_pepa.sm
-
78prism/src/pepa/src/TESTS/mobile.pepa
-
237prism/src/pepa/src/TESTS/mobile_pepa.sm
-
12prism/src/pepa/src/TESTS/small.pepa
-
45prism/src/pepa/src/TESTS/small_pepa.sm
-
8prism/src/pepa/src/compiler.sml
-
16prism/src/pepa/src/pepa.mlj
-
43prism/src/pepa/src/pepa.renamed.sml
-
23prism/src/pepa/src/sources.cm
@ -1,13 +0,0 @@ |
|||
(* |
|||
File: Alphabets.sig |
|||
|
|||
*) |
|||
signature Alphabets = |
|||
sig |
|||
|
|||
val lookup : string -> (string list * string list) option |
|||
|
|||
val recordActive : string * string list -> unit |
|||
val recordPassive : string * string list -> unit |
|||
|
|||
end; |
|||
@ -1,54 +0,0 @@ |
|||
(* |
|||
File: Alphabets.sml |
|||
|
|||
*) |
|||
structure Alphabets :> Alphabets = |
|||
struct |
|||
|
|||
type value = (string list * string list) ref |
|||
|
|||
datatype tree = empty | |
|||
node of tree ref * (string * value) * tree ref |
|||
|
|||
fun look (id, tree as ref empty) = NONE |
|||
| look (id, tree as ref (node (left, (id', value), right))) = |
|||
if id = id' |
|||
then SOME (!value) |
|||
else if id < id' then look (id, left) |
|||
else look (id, right) |
|||
|
|||
(* The data structure *) |
|||
val tree = ref empty |
|||
|
|||
(* This function is exported from this structure *) |
|||
fun lookup id = look (id, tree) |
|||
|
|||
fun find (id, f, tree as ref empty) = |
|||
let val newValue = ref ([], []) |
|||
in |
|||
f newValue; |
|||
tree := node (ref empty, (id, newValue), ref empty) |
|||
end |
|||
| find (id, f, tree as ref (node (left, (id', value), right))) = |
|||
if id = id' |
|||
then f (value) |
|||
else if id < id' then find (id, f, left) |
|||
else find (id, f, right) |
|||
|
|||
fun findAndReplace (id, f) = find (id, f, tree) |
|||
|
|||
fun addActive activeSet (r as ref (_, passiveSet)) = |
|||
r := (activeSet, passiveSet) |
|||
|
|||
(* This function is exported from this structure *) |
|||
fun recordActive (id, activeSet) = |
|||
findAndReplace (id, addActive activeSet) |
|||
|
|||
fun addPassive passiveSet (r as ref (activeSet, _)) = |
|||
r := (activeSet, passiveSet) |
|||
|
|||
(* This function is exported from this structure *) |
|||
fun recordPassive (id, passiveSet) = |
|||
findAndReplace (id, addPassive passiveSet) |
|||
|
|||
end; |
|||
@ -1,341 +0,0 @@ |
|||
GNU GENERAL PUBLIC LICENSE |
|||
Version 2, June 1991 |
|||
|
|||
Copyright (C) 1989, 1991 Free Software Foundation, Inc. |
|||
59 Temple Place - Suite 330 |
|||
Boston, MA 02111-1307, USA. |
|||
Everyone is permitted to copy and distribute verbatim copies |
|||
of this license document, but changing it is not allowed. |
|||
|
|||
Preamble |
|||
|
|||
The licenses for most software are designed to take away your |
|||
freedom to share and change it. By contrast, the GNU General Public |
|||
License is intended to guarantee your freedom to share and change free |
|||
software--to make sure the software is free for all its users. This |
|||
General Public License applies to most of the Free Software |
|||
Foundation's software and to any other program whose authors commit to |
|||
using it. (Some other Free Software Foundation software is covered by |
|||
the GNU Library General Public License instead.) You can apply it to |
|||
your programs, too. |
|||
|
|||
When we speak of free software, we are referring to freedom, not |
|||
price. Our General Public Licenses are designed to make sure that you |
|||
have the freedom to distribute copies of free software (and charge for |
|||
this service if you wish), that you receive source code or can get it |
|||
if you want it, that you can change the software or use pieces of it |
|||
in new free programs; and that you know you can do these things. |
|||
|
|||
To protect your rights, we need to make restrictions that forbid |
|||
anyone to deny you these rights or to ask you to surrender the rights. |
|||
These restrictions translate to certain responsibilities for you if you |
|||
distribute copies of the software, or if you modify it. |
|||
|
|||
For example, if you distribute copies of such a program, whether |
|||
gratis or for a fee, you must give the recipients all the rights that |
|||
you have. You must make sure that they, too, receive or can get the |
|||
source code. And you must show them these terms so they know their |
|||
rights. |
|||
|
|||
We protect your rights with two steps: (1) copyright the software, and |
|||
(2) offer you this license which gives you legal permission to copy, |
|||
distribute and/or modify the software. |
|||
|
|||
Also, for each author's protection and ours, we want to make certain |
|||
that everyone understands that there is no warranty for this free |
|||
software. If the software is modified by someone else and passed on, we |
|||
want its recipients to know that what they have is not the original, so |
|||
that any problems introduced by others will not reflect on the original |
|||
authors' reputations. |
|||
|
|||
Finally, any free program is threatened constantly by software |
|||
patents. We wish to avoid the danger that redistributors of a free |
|||
program will individually obtain patent licenses, in effect making the |
|||
program proprietary. To prevent this, we have made it clear that any |
|||
patent must be licensed for everyone's free use or not licensed at all. |
|||
|
|||
The precise terms and conditions for copying, distribution and |
|||
modification follow. |
|||
|
|||
GNU GENERAL PUBLIC LICENSE |
|||
TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION |
|||
|
|||
0. This License applies to any program or other work which contains |
|||
a notice placed by the copyright holder saying it may be distributed |
|||
under the terms of this General Public License. The "Program", below, |
|||
refers to any such program or work, and a "work based on the Program" |
|||
means either the Program or any derivative work under copyright law: |
|||
that is to say, a work containing the Program or a portion of it, |
|||
either verbatim or with modifications and/or translated into another |
|||
language. (Hereinafter, translation is included without limitation in |
|||
the term "modification".) Each licensee is addressed as "you". |
|||
|
|||
Activities other than copying, distribution and modification are not |
|||
covered by this License; they are outside its scope. The act of |
|||
running the Program is not restricted, and the output from the Program |
|||
is covered only if its contents constitute a work based on the |
|||
Program (independent of having been made by running the Program). |
|||
Whether that is true depends on what the Program does. |
|||
|
|||
1. You may copy and distribute verbatim copies of the Program's |
|||
source code as you receive it, in any medium, provided that you |
|||
conspicuously and appropriately publish on each copy an appropriate |
|||
copyright notice and disclaimer of warranty; keep intact all the |
|||
notices that refer to this License and to the absence of any warranty; |
|||
and give any other recipients of the Program a copy of this License |
|||
along with the Program. |
|||
|
|||
You may charge a fee for the physical act of transferring a copy, and |
|||
you may at your option offer warranty protection in exchange for a fee. |
|||
|
|||
2. You may modify your copy or copies of the Program or any portion |
|||
of it, thus forming a work based on the Program, and copy and |
|||
distribute such modifications or work under the terms of Section 1 |
|||
above, provided that you also meet all of these conditions: |
|||
|
|||
a) You must cause the modified files to carry prominent notices |
|||
stating that you changed the files and the date of any change. |
|||
|
|||
b) You must cause any work that you distribute or publish, that in |
|||
whole or in part contains or is derived from the Program or any |
|||
part thereof, to be licensed as a whole at no charge to all third |
|||
parties under the terms of this License. |
|||
|
|||
c) If the modified program normally reads commands interactively |
|||
when run, you must cause it, when started running for such |
|||
interactive use in the most ordinary way, to print or display an |
|||
announcement including an appropriate copyright notice and a |
|||
notice that there is no warranty (or else, saying that you provide |
|||
a warranty) and that users may redistribute the program under |
|||
these conditions, and telling the user how to view a copy of this |
|||
License. (Exception: if the Program itself is interactive but |
|||
does not normally print such an announcement, your work based on |
|||
the Program is not required to print an announcement.) |
|||
|
|||
These requirements apply to the modified work as a whole. If |
|||
identifiable sections of that work are not derived from the Program, |
|||
and can be reasonably considered independent and separate works in |
|||
themselves, then this License, and its terms, do not apply to those |
|||
sections when you distribute them as separate works. But when you |
|||
distribute the same sections as part of a whole which is a work based |
|||
on the Program, the distribution of the whole must be on the terms of |
|||
this License, whose permissions for other licensees extend to the |
|||
entire whole, and thus to each and every part regardless of who wrote it. |
|||
|
|||
Thus, it is not the intent of this section to claim rights or contest |
|||
your rights to work written entirely by you; rather, the intent is to |
|||
exercise the right to control the distribution of derivative or |
|||
collective works based on the Program. |
|||
|
|||
In addition, mere aggregation of another work not based on the Program |
|||
with the Program (or with a work based on the Program) on a volume of |
|||
a storage or distribution medium does not bring the other work under |
|||
the scope of this License. |
|||
|
|||
3. You may copy and distribute the Program (or a work based on it, |
|||
under Section 2) in object code or executable form under the terms of |
|||
Sections 1 and 2 above provided that you also do one of the following: |
|||
|
|||
a) Accompany it with the complete corresponding machine-readable |
|||
source code, which must be distributed under the terms of Sections |
|||
1 and 2 above on a medium customarily used for software interchange; or, |
|||
|
|||
b) Accompany it with a written offer, valid for at least three |
|||
years, to give any third party, for a charge no more than your |
|||
cost of physically performing source distribution, a complete |
|||
machine-readable copy of the corresponding source code, to be |
|||
distributed under the terms of Sections 1 and 2 above on a medium |
|||
customarily used for software interchange; or, |
|||
|
|||
c) Accompany it with the information you received as to the offer |
|||
to distribute corresponding source code. (This alternative is |
|||
allowed only for noncommercial distribution and only if you |
|||
received the program in object code or executable form with such |
|||
an offer, in accord with Subsection b above.) |
|||
|
|||
The source code for a work means the preferred form of the work for |
|||
making modifications to it. For an executable work, complete source |
|||
code means all the source code for all modules it contains, plus any |
|||
associated interface definition files, plus the scripts used to |
|||
control compilation and installation of the executable. However, as a |
|||
special exception, the source code distributed need not include |
|||
anything that is normally distributed (in either source or binary |
|||
form) with the major components (compiler, kernel, and so on) of the |
|||
operating system on which the executable runs, unless that component |
|||
itself accompanies the executable. |
|||
|
|||
If distribution of executable or object code is made by offering |
|||
access to copy from a designated place, then offering equivalent |
|||
access to copy the source code from the same place counts as |
|||
distribution of the source code, even though third parties are not |
|||
compelled to copy the source along with the object code. |
|||
|
|||
4. You may not copy, modify, sublicense, or distribute the Program |
|||
except as expressly provided under this License. Any attempt |
|||
otherwise to copy, modify, sublicense or distribute the Program is |
|||
void, and will automatically terminate your rights under this License. |
|||
However, parties who have received copies, or rights, from you under |
|||
this License will not have their licenses terminated so long as such |
|||
parties remain in full compliance. |
|||
|
|||
5. You are not required to accept this License, since you have not |
|||
signed it. However, nothing else grants you permission to modify or |
|||
distribute the Program or its derivative works. These actions are |
|||
prohibited by law if you do not accept this License. Therefore, by |
|||
modifying or distributing the Program (or any work based on the |
|||
Program), you indicate your acceptance of this License to do so, and |
|||
all its terms and conditions for copying, distributing or modifying |
|||
the Program or works based on it. |
|||
|
|||
6. Each time you redistribute the Program (or any work based on the |
|||
Program), the recipient automatically receives a license from the |
|||
original licensor to copy, distribute or modify the Program subject to |
|||
these terms and conditions. You may not impose any further |
|||
restrictions on the recipients' exercise of the rights granted herein. |
|||
You are not responsible for enforcing compliance by third parties to |
|||
this License. |
|||
|
|||
7. If, as a consequence of a court judgment or allegation of patent |
|||
infringement or for any other reason (not limited to patent issues), |
|||
conditions are imposed on you (whether by court order, agreement or |
|||
otherwise) that contradict the conditions of this License, they do not |
|||
excuse you from the conditions of this License. If you cannot |
|||
distribute so as to satisfy simultaneously your obligations under this |
|||
License and any other pertinent obligations, then as a consequence you |
|||
may not distribute the Program at all. For example, if a patent |
|||
license would not permit royalty-free redistribution of the Program by |
|||
all those who receive copies directly or indirectly through you, then |
|||
the only way you could satisfy both it and this License would be to |
|||
refrain entirely from distribution of the Program. |
|||
|
|||
If any portion of this section is held invalid or unenforceable under |
|||
any particular circumstance, the balance of the section is intended to |
|||
apply and the section as a whole is intended to apply in other |
|||
circumstances. |
|||
|
|||
It is not the purpose of this section to induce you to infringe any |
|||
patents or other property right claims or to contest validity of any |
|||
such claims; this section has the sole purpose of protecting the |
|||
integrity of the free software distribution system, which is |
|||
implemented by public license practices. Many people have made |
|||
generous contributions to the wide range of software distributed |
|||
through that system in reliance on consistent application of that |
|||
system; it is up to the author/donor to decide if he or she is willing |
|||
to distribute software through any other system and a licensee cannot |
|||
impose that choice. |
|||
|
|||
This section is intended to make thoroughly clear what is believed to |
|||
be a consequence of the rest of this License. |
|||
|
|||
8. If the distribution and/or use of the Program is restricted in |
|||
certain countries either by patents or by copyrighted interfaces, the |
|||
original copyright holder who places the Program under this License |
|||
may add an explicit geographical distribution limitation excluding |
|||
those countries, so that distribution is permitted only in or among |
|||
countries not thus excluded. In such case, this License incorporates |
|||
the limitation as if written in the body of this License. |
|||
|
|||
9. The Free Software Foundation may publish revised and/or new versions |
|||
of the General Public License from time to time. Such new versions will |
|||
be similar in spirit to the present version, but may differ in detail to |
|||
address new problems or concerns. |
|||
|
|||
Each version is given a distinguishing version number. If the Program |
|||
specifies a version number of this License which applies to it and "any |
|||
later version", you have the option of following the terms and conditions |
|||
either of that version or of any later version published by the Free |
|||
Software Foundation. If the Program does not specify a version number of |
|||
this License, you may choose any version ever published by the Free Software |
|||
Foundation. |
|||
|
|||
10. If you wish to incorporate parts of the Program into other free |
|||
programs whose distribution conditions are different, write to the author |
|||
to ask for permission. For software which is copyrighted by the Free |
|||
Software Foundation, write to the Free Software Foundation; we sometimes |
|||
make exceptions for this. Our decision will be guided by the two goals |
|||
of preserving the free status of all derivatives of our free software and |
|||
of promoting the sharing and reuse of software generally. |
|||
|
|||
NO WARRANTY |
|||
|
|||
11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY |
|||
FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN |
|||
OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES |
|||
PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED |
|||
OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF |
|||
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS |
|||
TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE |
|||
PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, |
|||
REPAIR OR CORRECTION. |
|||
|
|||
12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING |
|||
WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR |
|||
REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, |
|||
INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING |
|||
OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED |
|||
TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY |
|||
YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER |
|||
PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE |
|||
POSSIBILITY OF SUCH DAMAGES. |
|||
|
|||
END OF TERMS AND CONDITIONS |
|||
|
|||
How to Apply These Terms to Your New Programs |
|||
|
|||
If you develop a new program, and you want it to be of the greatest |
|||
possible use to the public, the best way to achieve this is to make it |
|||
free software which everyone can redistribute and change under these terms. |
|||
|
|||
To do so, attach the following notices to the program. It is safest |
|||
to attach them to the start of each source file to most effectively |
|||
convey the exclusion of warranty; and each file should have at least |
|||
the "copyright" line and a pointer to where the full notice is found. |
|||
|
|||
<one line to give the program's name and a brief idea of what it does.> |
|||
Copyright (C) 19yy <name of author> |
|||
|
|||
This program is free software; you can redistribute it and/or modify |
|||
it under the terms of the GNU General Public License as published by |
|||
the Free Software Foundation; either version 2 of the License, or |
|||
(at your option) any later version. |
|||
|
|||
This program is distributed in the hope that it will be useful, |
|||
but WITHOUT ANY WARRANTY; without even the implied warranty of |
|||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
|||
GNU General Public License for more details. |
|||
|
|||
You should have received a copy of the GNU General Public License |
|||
along with this program; see the file COPYING. If not, write to |
|||
the Free Software Foundation, Inc., 59 Temple Place - Suite 330, |
|||
Boston, MA 02111-1307, USA. |
|||
|
|||
Also add information on how to contact you by electronic and paper mail. |
|||
|
|||
If the program is interactive, make it output a short notice like this |
|||
when it starts in an interactive mode: |
|||
|
|||
Gnomovision version 69, Copyright (C) 19yy name of author |
|||
Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'. |
|||
This is free software, and you are welcome to redistribute it |
|||
under certain conditions; type `show c' for details. |
|||
|
|||
The hypothetical commands `show w' and `show c' should show the appropriate |
|||
parts of the General Public License. Of course, the commands you use may |
|||
be called something other than `show w' and `show c'; they could even be |
|||
mouse-clicks or menu items--whatever suits your program. |
|||
|
|||
You should also get your employer (if you work as a programmer) or your |
|||
school, if any, to sign a "copyright disclaimer" for the program, if |
|||
necessary. Here is a sample; alter the names: |
|||
|
|||
Yoyodyne, Inc., hereby disclaims all copyright interest in the program |
|||
`Gnomovision' (which makes passes at compilers) written by James Hacker. |
|||
|
|||
<signature of Ty Coon>, 1 April 1989 |
|||
Ty Coon, President of Vice |
|||
|
|||
This General Public License does not permit incorporating your program into |
|||
proprietary programs. If your program is a subroutine library, you may |
|||
consider it more useful to permit linking proprietary applications with the |
|||
library. If this is what you want to do, use the GNU Library General |
|||
Public License instead of this License. |
|||
@ -1,10 +0,0 @@ |
|||
(* |
|||
File: CommandLine.sig |
|||
|
|||
Used to compile the MLJ version of the Workbench only |
|||
*) |
|||
signature CommandLine = |
|||
sig |
|||
val setArguments : string list -> unit |
|||
val arguments : unit -> string list |
|||
end; |
|||
@ -1,15 +0,0 @@ |
|||
(* |
|||
File: CommandLine.sml |
|||
|
|||
Used to compile the MLJ version of the Workbench only |
|||
*) |
|||
structure CommandLine :> CommandLine = |
|||
struct |
|||
|
|||
val args = ref [] : string list ref |
|||
|
|||
fun setArguments s = args := s |
|||
|
|||
fun arguments () = !args |
|||
|
|||
end; |
|||
@ -1,18 +0,0 @@ |
|||
(* |
|||
File: Debugging.sig |
|||
|
|||
*) |
|||
signature Debugging = |
|||
sig |
|||
(* Check if the user has requested debugging information |
|||
by creating a file ".pepa_compiler_debug_true" in the |
|||
current working directory *) |
|||
val checkRequested : unit -> unit |
|||
|
|||
(* Flag set by the checkRequested function *) |
|||
val on : bool ref |
|||
|
|||
val log : string -> unit |
|||
val logList : string list -> unit |
|||
val logListList : string list list -> unit |
|||
end; |
|||
@ -1,39 +0,0 @@ |
|||
(* |
|||
File: Debugging.sml |
|||
*) |
|||
|
|||
structure Debugging :> Debugging = |
|||
struct |
|||
(* Flag set by the checkRequested function *) |
|||
val on = ref false |
|||
|
|||
(* Check if the user has requested debugging information |
|||
by creating a file ".pepa_compiler_debug_true" in the |
|||
current working directory *) |
|||
fun checkRequested () = |
|||
let val is = TextIO.openIn ".pepa_compiler_debug_true" |
|||
in on := true; |
|||
TextIO.closeIn is |
|||
end handle _ => on := false; |
|||
|
|||
fun say s = |
|||
if !on then |
|||
(TextIO.output(TextIO.stdErr, s); |
|||
TextIO.flushOut(TextIO.stdErr)) |
|||
else () |
|||
|
|||
fun log s = say ("DEBUGGING>> " ^ s ^ "\n") |
|||
|
|||
fun logList [] = say "\t*empty*\n" |
|||
| logList l = (say "\t[[["; logList' l ; say "]]]\n") |
|||
and logList' [] = () |
|||
| logList' [x] = say x |
|||
| logList' (x::xs) = (say x; say ", "; logList' xs) |
|||
|
|||
fun logListList [] = say "\t*empty*\n" |
|||
| logListList l = (say " [[[[[\n"; logListList' l ; say " ]]]]]\n") |
|||
and logListList' [] = () |
|||
| logListList' [x] = logList x |
|||
| logListList' (x::xs) = (logList x; say ",\n"; logListList' xs) |
|||
|
|||
end; |
|||
@ -1,12 +0,0 @@ |
|||
(* |
|||
File: Derivatives.sig |
|||
|
|||
*) |
|||
signature Derivatives = |
|||
sig |
|||
|
|||
val lookup : string -> string list option |
|||
|
|||
val recordDerivatives : string * string list -> unit |
|||
|
|||
end; |
|||
@ -1,47 +0,0 @@ |
|||
(* |
|||
File: Derivatives.sml |
|||
|
|||
*) |
|||
structure Derivatives :> Derivatives = |
|||
struct |
|||
|
|||
type value = string list ref |
|||
|
|||
datatype tree = empty | |
|||
node of tree ref * (string * value) * tree ref |
|||
|
|||
fun look (id, tree as ref empty) = NONE |
|||
| look (id, tree as ref (node (left, (id', value), right))) = |
|||
if id = id' |
|||
then SOME (!value) |
|||
else if id < id' then look (id, left) |
|||
else look (id, right) |
|||
|
|||
(* The data structure *) |
|||
val tree = ref empty |
|||
|
|||
(* This function is exported from this structure *) |
|||
fun lookup id = look (id, tree) |
|||
|
|||
fun find (id, f, tree as ref empty) = |
|||
let val newValue = ref [] |
|||
in |
|||
f newValue; |
|||
tree := node (ref empty, (id, newValue), ref empty) |
|||
end |
|||
| find (id, f, tree as ref (node (left, (id', value), right))) = |
|||
if id = id' |
|||
then f (value) |
|||
else if id < id' then find (id, f, left) |
|||
else find (id, f, right) |
|||
|
|||
fun findAndReplace (id, f) = find (id, f, tree) |
|||
|
|||
fun addDerivative derivativeSet r = |
|||
r := derivativeSet |
|||
|
|||
(* This function is exported from this structure *) |
|||
fun recordDerivatives (id, derivativeSet) = |
|||
findAndReplace (id, addDerivative derivativeSet) |
|||
|
|||
end; |
|||
@ -1,22 +0,0 @@ |
|||
(* |
|||
File: Error.sig |
|||
|
|||
Signature for the structure which prints PEPA semantic error messages. |
|||
*) |
|||
|
|||
signature Error = |
|||
sig |
|||
(* Thrown to stop the program *) |
|||
exception Fatal_error of string |
|||
|
|||
(* These functions never return *) |
|||
val fatal_error : string -> 'a |
|||
val internal_error : string -> 'a |
|||
val lexical_error : string -> 'a |
|||
val parse_error : string -> 'a |
|||
|
|||
(* Warning messages are printed only once *) |
|||
val warning : string -> unit |
|||
(* Reset this for testing purposes *) |
|||
val reset : unit -> unit |
|||
end; |
|||
@ -1,54 +0,0 @@ |
|||
(* |
|||
File: Error.sml |
|||
|
|||
Structure which prints PEPA semantic error messages. |
|||
*) |
|||
|
|||
structure Error |
|||
:> Error |
|||
= struct |
|||
exception Fatal_error of string |
|||
(* Generic error routine *) |
|||
fun error classification message = |
|||
let val diagnostic = classification ^ " error: " ^ message |
|||
in |
|||
(* Write errors to file for MLj version *) |
|||
if !Debugging.on |
|||
then let val errorlog = TextIO.openOut("pepacompiler.err") |
|||
in |
|||
TextIO.output (errorlog, ">> " ^ diagnostic ^ "\n"); |
|||
TextIO.flushOut errorlog; |
|||
TextIO.closeOut errorlog |
|||
end |
|||
else (); |
|||
raise Fatal_error (diagnostic) |
|||
end |
|||
|
|||
(* Fatal error messages *) |
|||
fun fatal_error s = error "Fatal" s |
|||
|
|||
(* Internal error messages *) |
|||
fun internal_error s = error "PEPA Workbench internal" s |
|||
|
|||
(* Syntax and parser error messages *) |
|||
fun lexical_error s = error "Lexical" s |
|||
fun parse_error s = error "Parsing" s |
|||
|
|||
(* Warning messages are not printed more than once, except |
|||
after a forced reset *) |
|||
local |
|||
val warningsSoFar = ref [] : string list ref |
|||
fun lookAndAdd (s, []) = (warningsSoFar := s :: !warningsSoFar; false) |
|||
| lookAndAdd (s, h::t) = s=h orelse lookAndAdd (s, t) |
|||
in |
|||
fun alreadyWarned s = lookAndAdd (s, !warningsSoFar) |
|||
fun reset () = warningsSoFar := [] |
|||
end |
|||
|
|||
fun warning s = |
|||
if alreadyWarned s then () else |
|||
(TextIO.output (TextIO.stdErr, |
|||
">> Warning: " ^ s ^ "\n"); |
|||
TextIO.flushOut TextIO.stdErr) |
|||
|
|||
end; |
|||
@ -1,11 +0,0 @@ |
|||
(* |
|||
File: Extractor.sig |
|||
|
|||
*) |
|||
signature Extractor = |
|||
sig |
|||
val finalise : unit -> unit |
|||
val initialise : string -> unit |
|||
val recordLocals : string * string list -> unit |
|||
val recordSystem : string -> unit |
|||
end; |
|||
@ -1,35 +0,0 @@ |
|||
(* |
|||
File: Extractor.sml |
|||
|
|||
*) |
|||
structure Extractor :> Extractor = |
|||
struct |
|||
val log = ref NONE : TextIO.outstream option ref |
|||
|
|||
(* Check if the user has requested logging information |
|||
by creating a file ".pepa_compiler_log_true" in the |
|||
current working directory *) |
|||
fun initialise jobname = |
|||
let val is = TextIO.openIn ".pepa_compiler_log_true" |
|||
in log := SOME (TextIO.openOut (jobname ^ ".log")); |
|||
TextIO.closeIn is |
|||
end handle _ => log := NONE; |
|||
|
|||
fun finalise() = case !log of NONE => () |
|||
| SOME os => TextIO.closeOut(os) |
|||
|
|||
fun print s = case !log of NONE => () |
|||
| SOME os => TextIO.output(os, s) |
|||
|
|||
fun listToString sep [] = "" |
|||
| listToString sep [x] = x |
|||
| listToString sep (x::xs) = x ^ sep ^ (listToString sep xs) |
|||
|
|||
fun recordLocals (component, localStates) = |
|||
print (component ^ " = {" ^ listToString ", " localStates ^ "}\n") |
|||
|
|||
fun recordSystem (system) = |
|||
print ("System = (" ^ system ^ ")\n") |
|||
|
|||
end; |
|||
|
|||
@ -1,17 +0,0 @@ |
|||
(* |
|||
File: Files.sig |
|||
|
|||
File handling for the PEPA Workbench |
|||
*) |
|||
|
|||
signature Files = |
|||
sig |
|||
|
|||
(* Read in a file, returning its contents, removing |
|||
comments while also processing any options *) |
|||
val readFile : string -> char list |
|||
|
|||
(* Get the job name *) |
|||
val jobName : unit -> string |
|||
|
|||
end; |
|||
@ -1,41 +0,0 @@ |
|||
(* |
|||
File: Files.sml |
|||
|
|||
File handling for the PEPA Workbench |
|||
*) |
|||
|
|||
structure Files |
|||
:> Files |
|||
= struct |
|||
|
|||
val job = ref "" |
|||
|
|||
fun jobName () = !job |
|||
|
|||
fun readFile s = |
|||
let |
|||
val reverse = implode o rev o explode |
|||
fun hasext s = String.isPrefix "apep." (reverse s) |
|||
val f = TextIO.openIn s handle _ => |
|||
TextIO.openIn (s^".pepa") handle _ => |
|||
if hasext s |
|||
then Error.fatal_error ("Cannot open \"" ^ s ^ "\"") |
|||
else Error.fatal_error ("Cannot open \"" ^ s ^ "\" or \"" ^ |
|||
s ^ ".pepa\"") |
|||
|
|||
val c = ref (SOME #" ") |
|||
val r = ref [] : char list ref |
|||
|
|||
fun prepend (ref NONE) = () |
|||
| prepend (ref (SOME c)) = r := c :: !r |
|||
in |
|||
job := s; |
|||
while (c := TextIO.input1 f; !c <> NONE) do |
|||
if !c = SOME #"%" (* Added comment syntax *) |
|||
then (TextIO.inputLine f; ()) |
|||
else prepend c; |
|||
TextIO.closeIn f; |
|||
rev (!r) |
|||
end |
|||
|
|||
end; |
|||
@ -1,5 +0,0 @@ |
|||
all: |
|||
javac pepa/compiler/*.java |
|||
|
|||
run: |
|||
java -classpath .:../pepa.zip pepa.compiler.Main ../TESTS/auction.pepa |
|||
@ -1,10 +0,0 @@ |
|||
package pepa.compiler; |
|||
|
|||
public class InternalError extends Exception { |
|||
private static final String flag = "\n[><] -----------> "; |
|||
|
|||
protected InternalError(String s) { |
|||
super(flag + flag + s + flag); |
|||
} |
|||
|
|||
} |
|||
@ -1,60 +0,0 @@ |
|||
package pepa.compiler; |
|||
|
|||
import java.lang.reflect.*; |
|||
public class Main { |
|||
|
|||
public static String compile(String fileName) throws InternalError { |
|||
try { |
|||
Class c = Class.forName("pepa"); |
|||
Method[] m = c.getMethods(); |
|||
// Terminate here if no methods found |
|||
if (m.length == 0) |
|||
throw new InternalError("Could not locate the methods for the PEPA compiler"); |
|||
|
|||
// Locate the entry point for the class |
|||
Method entryPoint = null; |
|||
for (int i = 0; i < m.length; i++) { |
|||
if (m[i].getName().equals("compile")) { |
|||
entryPoint = m[i]; |
|||
} |
|||
} |
|||
// Terminate here if the entry point was not found |
|||
if (entryPoint == null) |
|||
throw new InternalError("Could not locate the entry point for the PEPA compiler"); |
|||
|
|||
// Build the arguments for the method |
|||
Object[] oa = { fileName }; |
|||
Object o = entryPoint.invoke(null, oa); |
|||
if (!(o instanceof String)) |
|||
throw new InternalError("Non-string returned by PEPA compile method "); |
|||
|
|||
String PRISM_result = (String)o; |
|||
|
|||
return PRISM_result; |
|||
} catch (ClassNotFoundException cnfe) { |
|||
throw new InternalError("Could not load the PEPA compiler class from pepa.zip"); |
|||
} catch (SecurityException se) { |
|||
throw new InternalError("Could not secure the PEPA compiler class"); |
|||
} catch (IllegalAccessException iae) { |
|||
throw new InternalError("Could not access the PEPA compiler instance"); |
|||
} catch (IllegalArgumentException iarge) { |
|||
throw new InternalError("Attempted to start the PEPA compiler with the wrong arguments"); |
|||
} catch (InvocationTargetException ite) { |
|||
Throwable t = ite.getTargetException(); |
|||
throw new InternalError(t.toString()); |
|||
} |
|||
} |
|||
|
|||
public static void main(String[] args) throws InternalError { |
|||
if (args == null) |
|||
throw new InternalError("Cannot invoke the PEPA compiler on a null filename"); |
|||
|
|||
if (args.length == 0) |
|||
throw new InternalError("Must supply a file name to invoke the PEPA compiler"); |
|||
|
|||
if (args.length != 1) |
|||
throw new InternalError("Cannot invoke the PEPA compiler on more than one file"); |
|||
|
|||
System.out.println(compile(args[0])); |
|||
} |
|||
} |
|||
@ -1,18 +0,0 @@ |
|||
(* |
|||
File: Lexer.sig |
|||
|
|||
Functions which perform lexical analysis of PEPA models. |
|||
*) |
|||
|
|||
signature Lexer = |
|||
sig |
|||
|
|||
datatype token = |
|||
Ident of Pepa.Identifier |
|||
| Float of string |
|||
| Symbol of char |
|||
|
|||
val analyse : char list -> token list |
|||
|
|||
end; |
|||
|
|||
@ -1,46 +0,0 @@ |
|||
(* |
|||
File: Lexer.sml |
|||
|
|||
Structure which performs lexical analysis of PEPA models. |
|||
*) |
|||
|
|||
structure Lexer :> Lexer |
|||
= struct |
|||
datatype token = |
|||
Ident of Pepa.Identifier |
|||
| Float of string |
|||
| Symbol of char |
|||
|
|||
fun isIdChar c = Char.isAlphaNum c orelse Char.contains "'_*-" c |
|||
|
|||
fun isPepaSym c = Char.contains "/{}<>().,=+#;" c |
|||
|
|||
fun replace_T_by_infty "T" = "infty" |
|||
| replace_T_by_infty "top" = "infty" |
|||
| replace_T_by_infty s = s |
|||
|
|||
fun analyse [] = [] |
|||
| analyse (a::x) = |
|||
if Char.isSpace a then analyse x else |
|||
if isPepaSym a then Symbol a :: analyse x else |
|||
if Char.isDigit a then getnumber [a] x else |
|||
if Char.isAlpha a then getword [a] x else |
|||
Error.lexical_error ("Unrecognised token " |
|||
^ implode (a :: x)) |
|||
and getword l [] = [ident l] |
|||
| getword l (a::x) = |
|||
if isIdChar a |
|||
then getword (a::l) x |
|||
else ident l :: analyse (a::x) |
|||
and getnumber l [] = [float l] |
|||
| getnumber l (a::x) = |
|||
if Char.isDigit a orelse a = #"." |
|||
then getnumber (a::l) x |
|||
else float l :: analyse (a::x) |
|||
|
|||
and ident l = |
|||
Ident (replace_T_by_infty (implode (rev l))) |
|||
and float l = |
|||
Float (implode (rev l)) |
|||
|
|||
end; |
|||
@ -1,14 +0,0 @@ |
|||
(* |
|||
File: Lists.sig |
|||
|
|||
Operations on string lists |
|||
*) |
|||
|
|||
signature Lists = |
|||
sig |
|||
val addifmissing : string * string list -> string list |
|||
val insertu : string * string list -> string list |
|||
val merge : string list * string list -> string list |
|||
val sortu : string list -> string list |
|||
end; |
|||
|
|||
@ -1,28 +0,0 @@ |
|||
(* |
|||
File: Lists.sml |
|||
|
|||
Operations on string lists |
|||
*) |
|||
|
|||
structure Lists :> Lists = |
|||
struct |
|||
|
|||
fun sortu [] = [] |
|||
| sortu (h::t) = insertu (h, sortu t) |
|||
and insertu (x : string, []) = [x] |
|||
| insertu (x, h::t) = |
|||
if x < h then x :: h :: t else |
|||
if x = h then h :: t else h :: insertu (x, t); |
|||
|
|||
fun addifmissing (x : string, []) = [x] |
|||
| addifmissing (x, h::t) = if x=h then h::t else h :: addifmissing (x, t) |
|||
|
|||
fun merge ([], []) = [] : string list |
|||
| merge ([], l) = l |
|||
| merge (l, []) = l |
|||
| merge (l1 as (h1::t1), l2 as (h2::t2)) = |
|||
if h1 = h2 then merge (t1, l2) |
|||
else if h1 < h2 then h1 :: merge (t1, l2) |
|||
else h2 :: merge(l1, t2) |
|||
|
|||
end; |
|||
@ -1,13 +0,0 @@ |
|||
# A makefile for the PEPA to PRISM compiler
|
|||
|
|||
# Edit this line to locate your copy of the MLj compiler.
|
|||
#MLJ=/home/mlj/version-0.1/bin/mlj
|
|||
MLJ=/home/stg/pub/MLj/version-0.1/bin/mlj |
|||
|
|||
# The MLj compiler is available for download from
|
|||
# http://www.dcs.ed.ac.uk/home/mlj
|
|||
# if it is not installed on your system.
|
|||
|
|||
# You should not need to edit anything below this line.
|
|||
all: |
|||
${MLJ} pepa |
|||
@ -1,71 +0,0 @@ |
|||
# A makefile for the PEPA to PRISM compiler
|
|||
all: |
|||
/home/mlj/version-0.1/bin/mlj pepacompiler |
|||
javac -classpath pepacompiler.zip Test.java |
|||
java -classpath .:pepacompiler.zip Test |
|||
|
|||
|
|||
java: |
|||
export SAROOT=/home/stg/pub/pwb/COMPILER/0.021.4/JAVAsrc |
|||
export CLASSPATH=/home/java/jdk/jdk1.1.6/usr/local/opt/java1.1/lib/classes.zip:pepaMLj.zip |
|||
cp pepaMLj.zip JAVAsrc |
|||
cd JAVAsrc |
|||
unzip pepaMLj.zip |
|||
for i in *.class ; do \
|
|||
echo Decompiling $$i ... ; \
|
|||
/home/stg/SourceAgain/SourceAgain1.1/srcagain $$i > $$i.java ; \
|
|||
echo ; \
|
|||
done |
|||
|
|||
mosml: |
|||
mosmlc -c Debugging.sig |
|||
mosmlc -c Debugging.sml |
|||
mosmlc -c Error.sig |
|||
mosmlc -c Error.sml |
|||
mosmlc -c Files.sig |
|||
mosmlc -c Files.sml |
|||
mosmlc -c Pepa.sig |
|||
mosmlc -c Pepa.sml |
|||
mosmlc -c Lexer.sig |
|||
mosmlc -c Lexer.sml |
|||
mosmlc -c Parser.sig |
|||
mosmlc -c Parser.sml |
|||
mosmlc -c Sort.sig |
|||
mosmlc -c Sort.sml |
|||
mosmlc -c Semantic.sig |
|||
mosmlc -c Semantic.sml |
|||
mosmlc -c Prettyprinter.sig |
|||
mosmlc -c Prettyprinter.sml |
|||
mosmlc -c Lists.sig |
|||
mosmlc -c Lists.sml |
|||
mosmlc -c Derivatives.sig |
|||
mosmlc -c Derivatives.sml |
|||
mosmlc -c Alphabets.sig |
|||
mosmlc -c Alphabets.sml |
|||
mosmlc -c Extractor.sig |
|||
mosmlc -c Extractor.sml |
|||
mosmlc -c PEPA2PRISM.sig |
|||
mosmlc -c PEPA2PRISM.sml |
|||
# The following command produces a dynamically linked ELF binary
|
|||
mosmlc -o pepa2prism.linux-x86 compiler.sml |
|||
|
|||
static: |
|||
# the following command doesn't seem to work ...
|
|||
# this was an attempt to produce a statically linked ELF binary
|
|||
mosmlc -standalone -o pepa2prism.linux-x86-static compiler.sml |
|||
|
|||
clean: |
|||
rm *.ui *.uo |
|||
|
|||
m140: |
|||
mosmlc -o pepa2prism Int.uo Error.uo Options.uo Files.uo Pepa.uo Lexer.uo Prettyprinter.uo Parser.uo CommandLine.uo Sort.uo Semantic.uo PEPA2PRISM.uo Substring.uo Path.uo Time.uo OS.uo FileSys.uo Timer.uo Mosml.uo mosml140pepa2prism.sml |
|||
cat /usr/local/bin/camlrunm ./pepa2prism > pepa2prism.sun4-51 |
|||
chmod a+x pepa2prism.sun4-51 |
|||
|
|||
tests: |
|||
for i in TESTS/*.pepa ; do \
|
|||
echo pepa2prism.linux-x86 $$i ; \
|
|||
./pepa2prism.linux-x86 $$i ; \
|
|||
echo ; \
|
|||
done |
|||
|
|||
@ -1,15 +0,0 @@ |
|||
(* |
|||
File: PEPA2PRISM.sig |
|||
|
|||
*) |
|||
|
|||
signature PEPA2PRISM = |
|||
sig |
|||
(* The compile function is given a PEPA file name and |
|||
returns the equivalent PRISM model as a string *) |
|||
val compile : string -> string |
|||
|
|||
(* This is the main method which can be used if running |
|||
the compiler as a command-line application *) |
|||
val main : string list -> unit |
|||
end; |
|||
@ -1,771 +0,0 @@ |
|||
(* This is the PEPA-to-PRISM compiler *) |
|||
|
|||
structure PEPA2PRISM :> PEPA2PRISM = |
|||
struct |
|||
|
|||
val PEPA_version = "0.03.3 \"Inverleith Row\""; |
|||
val PEPA_compiled = "07-02-2003"; |
|||
val p2p as this_file = "PEPA2PRISM.sml"; |
|||
|
|||
val runningInteractively = ref false; |
|||
|
|||
fun println s = |
|||
if !runningInteractively |
|||
then (TextIO.output (TextIO.stdOut, s); |
|||
TextIO.flushOut TextIO.stdOut) |
|||
else () |
|||
|
|||
exception UndeclaredIdentifier of string |
|||
|
|||
fun lookup I [] = raise UndeclaredIdentifier (I) |
|||
| lookup I ((Id, P) :: t) = if I = Id then P else (lookup I t); |
|||
|
|||
fun member x [] = false |
|||
| member x (h::t) = (x=h) orelse (member x t); |
|||
|
|||
local |
|||
fun remove x [] = [] |
|||
| remove x (h::t) = if x=h then remove x t else h :: remove x t |
|||
in |
|||
infix minus |
|||
fun l minus [] = l |
|||
| l minus (h::t) = (remove h l) minus t; |
|||
end; |
|||
|
|||
exception Act of Pepa.Component and Pass of Pepa.Component; |
|||
|
|||
local |
|||
fun active E D (Pepa.PREFIX ((a, "infty"), P)) = active E D P |
|||
| active E D (Pepa.PREFIX ((a, r), P)) = Lists.insertu (a, active E D P) |
|||
| active E D (Pepa.CHOICE (P, Q)) = Lists.merge(active E D P, active E D Q) |
|||
| active E D (Pepa.HIDING (P, L)) = (active E D P) minus L |
|||
| active E D (Pepa.COOP (P, Q, L)) = Lists.merge (active E D P, active E D Q) |
|||
| active E D (Pepa.VAR I) = |
|||
if member I D then [] |
|||
else (* Look up a previously memoised result if possible *) |
|||
(case Alphabets.lookup I of |
|||
SOME (a as _::_, _) => a |
|||
| _ => let val activeSet = active E (I :: D) (lookup I E) |
|||
in Alphabets.recordActive(I, activeSet); |
|||
activeSet |
|||
end) |
|||
| active E D P = raise Act P |
|||
and passive E D (Pepa.PREFIX ((a, "infty"), P)) = Lists.insertu (a, passive E D P) |
|||
| passive E D (Pepa.PREFIX ((a, r), P)) = passive E D P |
|||
| passive E D (Pepa.CHOICE (P, Q)) = Lists.merge(passive E D P, passive E D Q) |
|||
| passive E D (Pepa.HIDING (P, L)) = (passive E D P) minus L |
|||
| passive E D (Pepa.COOP (P, Q, L)) = Lists.merge(passive E D P, passive E D Q) |
|||
minus L |
|||
| passive E D (Pepa.VAR I) = |
|||
if member I D then [] |
|||
else (* Look up a previously memoised result if possible *) |
|||
(case Alphabets.lookup I of |
|||
SOME (_, p as _::_) => p |
|||
| _ => let val passiveSet = passive E (I :: D) (lookup I E) |
|||
in Alphabets.recordPassive(I, passiveSet); |
|||
passiveSet |
|||
end) |
|||
| passive E D P = raise Pass P |
|||
and alphabet E D P = Lists.merge(active E D P, passive E D P) |
|||
in |
|||
fun act E D S = |
|||
let |
|||
val _ = Debugging.log "computing active set ... (act.1/2)" |
|||
val result = active E D S |
|||
val _ = Debugging.log "finished computing active set ... (act.2/2)" |
|||
in result end |
|||
fun pass E D S = |
|||
let |
|||
val _ = Debugging.log "computing passive set ... (pass.1/2)" |
|||
val result = passive E D S |
|||
val _ = Debugging.log "finished computing passive set ... (pass.2/2)" |
|||
in result end |
|||
fun alph E D S = |
|||
let |
|||
val _ = Debugging.log "computing alphabet ... (alph.1/2)" |
|||
val result = alphabet E D S |
|||
val _ = Debugging.log "finished computing alphabet ... (alph.2/2)" |
|||
in result end |
|||
end |
|||
|
|||
exception Modules of Pepa.Component |
|||
fun modules E D (Pepa.PREFIX (_, P)) = [] |
|||
| modules E D (Pepa.CHOICE (P, Q)) = [] |
|||
| modules E D (Pepa.HIDING (P, L)) = (modules E D P) |
|||
| modules E D (Pepa.COOP (Pepa.VAR P, Pepa.VAR Q, L)) = |
|||
(P :: |
|||
(if member P D then [] else modules E (P :: Q :: D) (lookup P E))) @ |
|||
(Q :: |
|||
(if member Q D then [] else modules E (P :: Q :: D) (lookup Q E))) |
|||
| modules E D (Pepa.COOP (Pepa.VAR P, Q, L)) = |
|||
(P :: |
|||
(if member P D then [] else modules E (P :: D) (lookup P E))) @ |
|||
modules E (P :: D) Q |
|||
| modules E D (Pepa.COOP (P, Pepa.VAR Q, L)) = |
|||
modules E (Q :: D) P @ |
|||
(if member Q D then [] else modules E (Q :: D) (lookup Q E)) @ |
|||
[Q] |
|||
| modules E D (Pepa.COOP (P, Q, L)) = |
|||
modules E D P @ modules E D Q |
|||
| modules E D (Pepa.VAR I) = [I] |
|||
| modules E D P = raise Modules P; |
|||
|
|||
local |
|||
fun addifmissing (x, []) = [x] |
|||
| addifmissing (x, h::t) = if x=h then h::t else h :: addifmissing (x, t) |
|||
fun duplicates [] = [] |
|||
| duplicates (h :: t) = |
|||
if member h t |
|||
then addifmissing (h, duplicates t) |
|||
else duplicates t |
|||
in fun moduletypes E _ P = duplicates (modules E [] P) |
|||
end |
|||
|
|||
(* module specifications --- find the module and work out *) |
|||
|
|||
infix intersect |
|||
fun [] intersect l = [] |
|||
| (h::t) intersect l = |
|||
if member h l then h :: (t intersect l) else t intersect l |
|||
|
|||
fun spec E System Module = |
|||
let |
|||
val A = act E [] (Pepa.VAR Module) |
|||
|
|||
(* Cool function definition. Read the @ symbol as `union'. *) |
|||
fun sp (Pepa.COOP (P, Q, L)) coopset = |
|||
(if P = Pepa.VAR Module orelse Q = Pepa.VAR Module |
|||
then (A intersect L) @ (A intersect coopset) |
|||
else []) @ |
|||
(sp P (coopset @ L)) @ |
|||
(sp Q (coopset @ L)) |
|||
|
|||
| sp (Pepa.HIDING (P, L)) coopset = |
|||
(if P = Pepa.VAR Module |
|||
then ((coopset minus L) intersect A) |
|||
else []) @ |
|||
sp P (coopset minus L) |
|||
|
|||
| sp _ _ = [] |
|||
|
|||
in Lists.sortu (sp System []) |
|||
end |
|||
|
|||
local |
|||
fun derivs E D (Pepa.PREFIX (_, P)) = derivs E D P |
|||
| derivs E D (Pepa.CHOICE (P, Q)) = |
|||
Lists.merge (derivs E D P, derivs E D Q) |
|||
| derivs E D (Pepa.HIDING (P, L)) = derivs E D P |
|||
| derivs E D (Pepa.VAR P) = |
|||
if member P D then D |
|||
else derivs E (Lists.insertu (P, D)) (lookup P E) |
|||
(* |
|||
(* Lookup a previously memoised result if possible *) |
|||
(case Derivatives.lookup P of |
|||
SOME ds => ds |
|||
| _ => let val derivativeSet = derivs E (Lists.insertu (P, D)) (lookup P E) |
|||
in Derivatives.recordDerivatives(P, derivativeSet); |
|||
derivativeSet |
|||
end) |
|||
*) |
|||
| derivs _ D _ = D |
|||
in |
|||
fun derivatives E D s = derivs E D (lookup s E) |
|||
end; |
|||
(* *) |
|||
type SystemSpecification = |
|||
{ activity_names : string list, |
|||
derivative_names : string list, |
|||
entries : string list, |
|||
name : Pepa.Identifier, |
|||
rpc_names : string list } |
|||
type Analysis = |
|||
{ active : string list, |
|||
concurrency : Pepa.Identifier list, |
|||
passive : string list, |
|||
system : SystemSpecification list, |
|||
modules : string list, |
|||
moduletypes : Pepa.Identifier list } |
|||
(* *) |
|||
local |
|||
fun analyse E (Pepa.CONSTS (I, P, L)) = analyse ((I, P) :: E) L |
|||
| analyse E P = |
|||
let |
|||
val _ = Debugging.log "inside analysis, computing modules ... (analyse.1/7)" |
|||
val modules_P = modules E [] P |
|||
val _ = Debugging.log "inside analysis, sorting module results ... (analyse.2/7)" |
|||
val modules_P' = Lists.sortu modules_P |
|||
val _ = Debugging.log "inside analysis, computing module types ... (analyse.3/7)" |
|||
val moduletypes_P = moduletypes E [] P |
|||
val _ = Debugging.log "inside analysis, finished computing module types ... (analyse.4/7)" |
|||
fun module_analyse s = |
|||
let |
|||
val _ = Debugging.log "inside module analysis ... (module_analyse.1/3)" |
|||
val own_entries = spec E P s |
|||
val _ = Debugging.log "inside module analysis ... (module_analyse.2/3)" |
|||
val derivs = derivatives E [] s |
|||
val _ = Debugging.log "inside module analysis ... (module_analyse.3/3)" |
|||
in |
|||
{ name = s, |
|||
entries = own_entries, |
|||
derivative_names = derivs, |
|||
activity_names = (act E [] (Pepa.VAR s)) |
|||
minus ("tau" :: own_entries), |
|||
rpc_names = (pass E [] (Pepa.VAR s)) |
|||
} |
|||
end |
|||
val _ = Debugging.log "inside analysis, starting computing found modules ... (analyse.5/7)" |
|||
val found_modules = modules_P' minus moduletypes_P |
|||
val _ = Debugging.log "inside analysis, finished computing found modules ... (analyse.6/7)" |
|||
val _ = Debugging.log "modules_P' is: ... " |
|||
val _ = Debugging.logList modules_P' |
|||
val _ = Debugging.log "... end modules_P'" |
|||
val found_system = map module_analyse modules_P' |
|||
val _ = Debugging.log "derivative names are: ... " |
|||
val _ = Debugging.logListList (map #derivative_names found_system) |
|||
val _ = Debugging.log "... end derivative names" |
|||
val _ = Debugging.log "inside analysis, finished computing found modules ... (analyse.7/7)" |
|||
in { active = (act E [] P) minus ["tau"], |
|||
passive = pass E [] P, |
|||
concurrency = modules_P, |
|||
modules = found_modules, |
|||
moduletypes = moduletypes_P, |
|||
system = found_system |
|||
} |
|||
end |
|||
in |
|||
val analyse : Pepa.Component -> Analysis = analyse [] |
|||
end; |
|||
(* *) |
|||
fun named [] = true |
|||
| named ((Pepa.PREFIX (_, Pepa.VAR _)) :: t) = named t |
|||
| named _ = false; |
|||
|
|||
exception Find |
|||
local |
|||
fun duplicates [] = [] |
|||
| duplicates (h::t) = if member h t then h :: duplicates t else duplicates t |
|||
fun get_name (Pepa.PREFIX ((a, _), _)) = a |
|||
| get_name _ = "" |
|||
fun choices E D (Pepa.PREFIX ((a, "infty"), _)) = [] |
|||
| choices E D (P as (Pepa.PREFIX ((a, _), _))) = [P] |
|||
| choices E D (Pepa.CHOICE (P, Q)) = |
|||
(choices E D P) @ (choices E D Q) |
|||
| choices E D (Pepa.VAR P) = |
|||
if member P D then [] else choices E (P :: D) (lookup P E) |
|||
| choices _ _ _ = [] |
|||
val filter = Lists.sortu o duplicates o (map get_name) |
|||
fun poss_choices E D P = filter (choices E D P) |
|||
fun choosy E P = |
|||
let val _ = Debugging.log "entered choosy function ... (choosy.1/4)" |
|||
val C = choices E [] P |
|||
val _ = Debugging.log "evaluated choices ... (choosy.2/4)" |
|||
val C' = filter C |
|||
val _ = Debugging.log "filtered component list ... (choosy.3/4)" |
|||
val activities = act E [] P |
|||
val _ = Debugging.log "computed activities.... (choosy.4/4)" |
|||
in (C' intersect activities) <> [] andalso (not (named C)) |
|||
end |
|||
fun any [] = false |
|||
| any (h :: t) = h orelse any t |
|||
|
|||
fun find_in_system [] P = raise Find |
|||
| find_in_system ((h : SystemSpecification) :: t) P = |
|||
if #name(h) = P then h else find_in_system t P |
|||
|
|||
fun module_is_choosy E (A : Analysis) P = |
|||
let val _ = Debugging.log "finding choosy modules ... (module_is_choosy.1/4)" |
|||
val derivativeNames = #derivative_names (find_in_system (#system A) P) |
|||
val _ = Debugging.log "found derivative names ... (module_is_choosy.2/4)" |
|||
val derivativeIdentifiers = map Pepa.VAR derivativeNames |
|||
val _ = Debugging.log "constructed derivative identifiers ... (module_is_choosy.3/4)" |
|||
val anyTrue = any (map (choosy E) derivativeIdentifiers) |
|||
val _ = Debugging.log "finding any choosy module ... (module_is_choosy.4/4)" |
|||
in |
|||
anyTrue |
|||
end |
|||
|
|||
fun env (Pepa.CONSTS (I, P, L)) = (I, P) :: env L |
|||
| env _ = [] |
|||
in |
|||
fun find_choosy_modules A S = |
|||
let |
|||
val _ = Debugging.log "finding choosy modules ... (find_choosy_modules.1/1)" |
|||
val E = env S |
|||
fun f [] = [] |
|||
| f (h::t) = if module_is_choosy E A h then h :: f t else f t |
|||
in f end |
|||
|
|||
fun single_choice [] = true |
|||
| single_choice [_] = true |
|||
| single_choice ((Pepa.PREFIX ((a, _), _)) :: (t as ((Pepa.PREFIX ((b, _), _)) :: _))) = |
|||
a=b andalso single_choice t |
|||
| single_choice _ = false |
|||
end; |
|||
(* *) |
|||
exception Lookup; |
|||
exception Markup; |
|||
exception Comms |
|||
(* *) |
|||
fun spandex name = |
|||
let fun dropnum [] = [] |
|||
| dropnum (name as h::t) = |
|||
if Char.isDigit h then dropnum t else name |
|||
in (implode o rev o tl o dropnum o rev o explode) name |
|||
end |
|||
|
|||
fun compute_id name = |
|||
let fun getnum [] = [] |
|||
| getnum (h::t) = |
|||
if Char.isDigit h then h :: getnum t else [] |
|||
in (implode o rev o getnum o rev o explode) name |
|||
end |
|||
|
|||
fun lookup2 [] P = raise Lookup |
|||
| lookup2 ({activity_names, derivative_names, entries, name, rpc_names} :: t) P = |
|||
if name = P orelse name = spandex P |
|||
then {entries = entries, name = P, rpc_names = rpc_names} |
|||
else lookup2 t P |
|||
(* *) |
|||
(* The markup function only processes parallel components *) |
|||
fun markup moduletypes P = |
|||
let fun skull (Pepa.CONSTS (I, P, L)) = skull L |
|||
| skull P = P |
|||
fun nextindex P [] = 0 |
|||
| nextindex P ((P', n) :: t) = |
|||
if P = P' then n else nextindex P t |
|||
fun mk E (Pepa.HIDING (P, L)) = |
|||
let val (E', P') = mk E P in (E', Pepa.HIDING (P', L)) end |
|||
| mk E (Pepa.COOP (P, Q, L)) = |
|||
let val (E', P') = mk E P |
|||
val (E'', Q') = mk E' Q |
|||
in (E'', Pepa.COOP (P', Q', L)) |
|||
end |
|||
| mk E (Pepa.VAR P) = |
|||
if member P moduletypes |
|||
then let val m = nextindex P E |
|||
in ((P, m+1) :: E, Pepa.VAR (P ^ "_" ^ Int.toString m)) |
|||
end |
|||
else (E, Pepa.VAR P) |
|||
| mk _ _ = raise Markup |
|||
in #2 (mk [] (skull P)) |
|||
end |
|||
(* *) |
|||
local |
|||
fun partners P a [] = [] |
|||
| partners P a ({ active, activity, passive } :: t) = |
|||
if passive = P andalso activity = a then |
|||
active :: partners P a t |
|||
else |
|||
partners P a t |
|||
in |
|||
val partners = fn comms => fn P => fn a => partners P a comms |
|||
end |
|||
(* *) |
|||
local |
|||
fun partners P a [] = [] |
|||
| partners P a ({ active, activity, passive } :: t) = |
|||
if spandex passive = P andalso activity = a then |
|||
(active, compute_id passive) :: partners P a t |
|||
else |
|||
partners P a t |
|||
in |
|||
val partners_in_modules = fn comms => fn P => fn a => partners P a comms |
|||
end |
|||
(* *) |
|||
|
|||
fun internalise L s = |
|||
let fun int {entries, name, rpc_names} = |
|||
{ entries = entries minus L, |
|||
name = name, |
|||
rpc_names = rpc_names minus L } |
|||
in map int s |
|||
end |
|||
|
|||
|
|||
fun postanalyse |
|||
({ active, passive, concurrency, modules, moduletypes, system } : Analysis) P = |
|||
let val markP = markup moduletypes P |
|||
|
|||
(* The comms function only processes parallel components *) |
|||
fun comms (Pepa.VAR P) = ([lookup2 system P], []) |
|||
| comms (Pepa.HIDING (P, L)) = |
|||
let val (table, results) = comms P |
|||
in (internalise L table, results) |
|||
end |
|||
| comms (Pepa.COOP (P, Q, L)) = |
|||
let val (tableP, resultsP) = comms P |
|||
val (tableQ, resultsQ) = comms Q |
|||
in (tableP @ tableQ, |
|||
resultsP @ resultsQ @ connect (tableP, tableQ, L)) |
|||
end |
|||
| comms _ = raise Comms |
|||
and connect ( _, _, []) = [] |
|||
| connect ([], _, _) = [] |
|||
| connect ( _, [], _) = [] |
|||
| connect ({ entries = eP, name = P, rpc_names = rP } :: tableP, tableQ, L) = |
|||
let fun cp { entries = eQ, name = Q, rpc_names = rQ } = |
|||
let fun PtoQ name = { passive = P, activity = name, active = Q } |
|||
fun QtoP name = { passive = Q, activity = name, active = P } |
|||
in map PtoQ ((rP intersect eQ) intersect L) @ |
|||
map QtoP ((rQ intersect eP) intersect L) |
|||
end |
|||
in map cp tableQ @ connect (tableP, tableQ, L) |
|||
end |
|||
|
|||
fun flatten [] = [] |
|||
| flatten (h::t) = h @ flatten t |
|||
|
|||
in (flatten o #2 o comms) markP |
|||
end |
|||
|
|||
|
|||
(* The activeActive function only processes parallel components *) |
|||
fun activeActive system (Pepa.CONSTS (_, _, L)) = activeActive system L |
|||
| activeActive system (Pepa.VAR P) = ([lookup2 system P], []) |
|||
| activeActive system (Pepa.HIDING (P, L)) = |
|||
let val (table, results) = activeActive system P |
|||
in (internalise L table, results) |
|||
end |
|||
| activeActive system (Pepa.COOP (P, Q, L)) = |
|||
let val (tableP, resultsP) = activeActive system P |
|||
val (tableQ, resultsQ) = activeActive system Q |
|||
in (tableP @ tableQ, |
|||
resultsP @ resultsQ @ connect (tableP, tableQ, L)) |
|||
end |
|||
| activeActive system _ = Error.internal_error ("Active/active function code") |
|||
and connect ( _, _, []) = [] |
|||
| connect ([], _, _) = [] |
|||
| connect ( _, [], _) = [] |
|||
| connect ({ entries = eP, name = P, rpc_names = rP } :: tableP, tableQ, L) = |
|||
let fun cp { entries = eQ, name = Q, rpc_names = rQ } = |
|||
eP intersect eQ intersect L |
|||
in map cp tableQ @ connect (tableP, tableQ, L) |
|||
end |
|||
|
|||
|
|||
|
|||
infix ^^ |
|||
fun s1 ^^ s2 = s1 ^ "\n" ^ s2 |
|||
infix & |
|||
fun s & "" = s |
|||
| s & t = s ^^ t |
|||
infix && |
|||
fun "" && "" = "" |
|||
| s && "" = s |
|||
| "" && t = t |
|||
| s && t = s ^^ "" ^^ t |
|||
|
|||
fun translate P jobname = |
|||
let |
|||
val _ = Debugging.log "inside translation function (translate.1)" |
|||
val analysis as { active, passive, concurrency, modules, moduletypes, system } = |
|||
analyse P |
|||
val _ = Debugging.logList active; |
|||
val _ = Debugging.logList passive; |
|||
val _ = Debugging.logList modules; |
|||
val _ = Debugging.logList moduletypes; |
|||
val _ = Debugging.log "inside translation function (translate.2)" |
|||
|
|||
fun strList [] = "" |
|||
| strList [x] = quote x |
|||
| strList (h::t) = quote h ^ ", " ^ strList t |
|||
and quote s = "``" ^ s ^ "''" |
|||
val _ = Debugging.log "inside translation function (translate.3)" |
|||
val _ = case List.concat (#2 (activeActive system P)) of |
|||
[] => () |
|||
| aa => Error.warning |
|||
("Active/active synchronisation found on " ^ |
|||
strList (Lists.sortu aa)) |
|||
|
|||
val _ = Debugging.log "inside translation function (translate.4)" |
|||
|
|||
val choosy_modules : Pepa.Identifier list = find_choosy_modules analysis P modules |
|||
val _ = Debugging.logList choosy_modules; |
|||
|
|||
val _ = Debugging.log "inside translation function (translate.5)" |
|||
val comms = postanalyse analysis P |
|||
val _ = Debugging.log "inside translation function (translate.6)" |
|||
val partners : string -> string -> string list = partners comms |
|||
val _ = Debugging.log "inside translation function (translate.7)" |
|||
val partners_in_modules = partners_in_modules comms |
|||
|
|||
val _ = Debugging.log "inside translation function (translate.8)" |
|||
|
|||
fun select _ P [] = [] |
|||
| select f P ((h as { name, entries, |
|||
derivative_names, |
|||
activity_names, |
|||
rpc_names }) :: t) = |
|||
if name = P then f h else select f P t |
|||
fun interface P l = select #entries P l |
|||
fun entries [] = "" |
|||
| entries (h::t) = "// activity " ^ h ^^ entries t |
|||
fun modulespecs qualifier [] = "" |
|||
| modulespecs qualifier (h::t) = |
|||
qualifier ^ h ^ |
|||
(case interface h system of |
|||
[] => " empty: only individual or passive activities" | |
|||
l => "" ^^ |
|||
entries l ^ "// endinterface ") ^^ |
|||
modulespecs qualifier t |
|||
|
|||
local |
|||
fun body (myModuleName as T, myModuleNumber as 1) P = |
|||
let |
|||
val names = select #derivative_names T system |
|||
val procs = select #activity_names T system |
|||
val singular = length names = 1 |
|||
val state = T ^ "_STATE" |
|||
fun define module [] = "" |
|||
| define module [x] = |
|||
"// This module has only one local state even" ^^ |
|||
"// though we write the variable range as [0..1]" ^^ |
|||
"const " ^ module ^ " = 0;" ^^ |
|||
"module " ^ module ^^ |
|||
"" ^^ |
|||
" " ^ state ^ " : [0..1] init 0;" ^^ |
|||
"" |
|||
| define module l = |
|||
let |
|||
fun csep n [] = "" |
|||
| csep n [x] = fmt n x |
|||
| csep n (h :: t) = fmt n h ^ ";\nconst " ^ csep (n + 1) t |
|||
and fmt n s = s ^ " = " ^ Int.toString n |
|||
in |
|||
"// Descriptive names for the local states of" ^^ |
|||
"// this module, taken from the PEPA input model" ^^ |
|||
"const " ^ csep 0 l ^ ";" ^^ |
|||
"module " ^ module ^^ |
|||
"" ^^ |
|||
" " ^ state ^ " : [0.." ^ Int.toString(length l - 1) ^ "] init " ^ T ^ ";" ^^ |
|||
"" |
|||
end |
|||
|
|||
fun sortagent E passives = |
|||
let |
|||
fun sort (Pepa.VAR I) = sort (lookup I E) |
|||
| sort (P as (Pepa.PREFIX ((a, r), _))) = |
|||
if member a ("tau" :: passives) |
|||
then ([], [], [P]) |
|||
else if r = "infty" |
|||
then ([], [P], []) |
|||
else ([P], [], []) |
|||
| sort (Pepa.CHOICE (P, Q)) = |
|||
let val ((accept1, call1, pcall1), |
|||
(accept2, call2, pcall2)) = (sort P, sort Q) |
|||
in (accept1 @ accept2, call1 @ call2, pcall1 @ pcall2) |
|||
end |
|||
| sort _ = ([], [], []) |
|||
in |
|||
sort |
|||
end |
|||
|
|||
fun trsing sep fmt = |
|||
let |
|||
fun tr E (Pepa.CONSTS (I, P, L)) T = tr ((I, P) :: E) L T |
|||
| tr E _ T = |
|||
let |
|||
fun trsys sep (Pepa.CHOICE (P,Q)) = |
|||
trsys sep P ^^ trsys sep Q |
|||
| trsys sep (Pepa.PREFIX (("tau", "infty"), Pepa.VAR I)) = |
|||
((* A passive action cannot be synchronised upon. *) |
|||
Error.warning ("Cannot synchronise on a tau action: should not be passive"); |
|||
fmt "" "1" I) |
|||
| trsys sep (Pepa.PREFIX (("tau", r), Pepa.VAR I)) = |
|||
(* It's OK to have a tau move if the rate is not infty *) |
|||
fmt "" r I |
|||
| trsys sep (P as Pepa.PREFIX ((a, "infty"), Pepa.VAR I)) = |
|||
((* All passive actions should be matched. We generate |
|||
a warning for this, but we could classify it as an error |
|||
Note that we check the term, T, not the derivative I. *) |
|||
if !Debugging.on andalso |
|||
partners T a = [] andalso partners_in_modules T a = [] |
|||
then Error.warning ("unmatched passive action: " ^ a) |
|||
else (); |
|||
fmt a "1" I) |
|||
| trsys sep (Pepa.PREFIX ((a, r), Pepa.VAR I)) = |
|||
((* PEPA and PRISM do different things with active/active |
|||
synchronisation but we have previously trapped this *) |
|||
fmt a r I) |
|||
| trsys sep _ = |
|||
Error.fatal_error "Composition/hiding found in component defn" |
|||
in trsys sep (lookup T E) |
|||
end |
|||
in tr |
|||
end |
|||
|
|||
fun trcase sep names E P T = |
|||
let |
|||
fun trclause [] = "" |
|||
| trclause (h::t) = |
|||
let |
|||
fun fmt stateID state action rate newstate = |
|||
" " ^ |
|||
"[" ^ action ^ "] (" ^ stateID ^ "=" ^ state ^ ") -> " ^ |
|||
rate ^ " : (" ^ stateID ^ "'=" ^ newstate ^ ");" |
|||
in |
|||
trsing (sep ^ " ") (fmt state h) E P h ^^ |
|||
trclause t |
|||
end |
|||
in trclause names |
|||
end |
|||
|
|||
val _ = Extractor.recordLocals (T, names) |
|||
in |
|||
define T names ^^ |
|||
trcase " " names [] P T ^^ |
|||
"endmodule" ^^ "" |
|||
end |
|||
| body (myModuleName as T, myModuleNumber as n) P = |
|||
let |
|||
val thisCopy = T ^ "_" ^ Int.toString n |
|||
in |
|||
"// We make another copy of module " ^ T ^^ |
|||
"module " ^ thisCopy ^ " = " ^ |
|||
T ^ "[" ^ T ^ "_STATE=" ^ thisCopy ^ "_STATE]\nendmodule\n" |
|||
end |
|||
in |
|||
fun modulebodies [] _ = "" |
|||
| modulebodies [h] P = body h P |
|||
| modulebodies (h::t) P = |
|||
body h P ^^ modulebodies t P |
|||
end |
|||
fun systemEquation P = |
|||
let |
|||
fun root (Pepa.CONSTS (I, P, L)) = root L |
|||
| root P = P |
|||
val extractorString = Prettyprinter.print Prettyprinter.uncompressed (root P) |
|||
val _ = Extractor.recordSystem extractorString |
|||
in |
|||
"// The system equation" ^^ |
|||
"system" ^^ |
|||
" " ^ |
|||
Prettyprinter.print Prettyprinter.asPRISM P ^^ |
|||
"endsystem" |
|||
end |
|||
|
|||
fun rates (Pepa.CONSTS (I, Pepa.RATE(r), P)) = |
|||
"rate " ^ I ^ " = " ^ r ^ ";" ^^ rates P |
|||
| rates (Pepa.CONSTS (I, _, P)) = |
|||
rates P |
|||
| rates _ = "" |
|||
|
|||
local |
|||
val l : string list ref = ref [] |
|||
fun countList I [] = 0 |
|||
| countList I (h::t) = (if I = h then 1 else 0) + countList I t |
|||
in |
|||
fun count I = (l := I :: !l; countList I (!l)) |
|||
end |
|||
|
|||
fun flatten (Pepa.CONSTS (I, P, L)) = flatten L |
|||
| flatten (Pepa.HIDING (P, L)) = flatten P |
|||
| flatten (Pepa.COOP (P, Q, L)) = flatten P @ flatten Q |
|||
| flatten (Pepa.VAR (I)) = [(I, count I)] |
|||
| flatten _ = Error.internal_error ("Prefix/choice found in PEPA system equation") |
|||
|
|||
val _ = Debugging.log "inside translation function (4)" |
|||
|
|||
in |
|||
"// Output from the PEPA-to-PRISM compiler" ^^ |
|||
"// Version "^ PEPA_version ^^ |
|||
"// Released: " ^ PEPA_compiled ^^ |
|||
"// " ^^ |
|||
"// Model file: " ^ jobname ^^ |
|||
(* |
|||
The Date structure is not available under Moscow ML 1.40 |
|||
"// Compiled: " ^ Date.fmt "%c" (Date.fromTimeLocal (Time.now())) ^^ |
|||
*) |
|||
|
|||
"" ^^ |
|||
"// All PEPA models define CTMCs so mark this as a stochastic model " ^^ |
|||
"stochastic" && |
|||
"// The rates used in the model " ^^ |
|||
rates P && |
|||
|
|||
"// Information about components inferred by the compiler" ^^ |
|||
"// during static analysis:" ^^ |
|||
"//" ^^ |
|||
modulespecs "// interface " modules ^^ |
|||
modulespecs "// interface " moduletypes && |
|||
|
|||
modulebodies (flatten P) P && |
|||
systemEquation P && |
|||
"// End of output from the PEPA-to-PRISM compiler\n" |
|||
end |
|||
|
|||
|
|||
local |
|||
fun rmext (#"\n" :: t) = rmext t |
|||
| rmext (#"a" :: #"p" :: #"e" :: #"p" :: #"." :: t) = implode (rev t) |
|||
| rmext other = implode (rev other) |
|||
in |
|||
fun removeExtension s = rmext (rev (explode s)) |
|||
end |
|||
|
|||
fun startsWithHyphen [] = false |
|||
| startsWithHyphen (#"-" :: _) = true |
|||
| startsWithHyphen _ = false |
|||
|
|||
fun isNotFlag s = not (startsWithHyphen (explode s)) |
|||
|
|||
val nonFlagArgs = List.filter isNotFlag |
|||
|
|||
fun getJobName args = |
|||
case nonFlagArgs args of |
|||
[x] => removeExtension x |
|||
| _ => (TextIO.output (TextIO.stdOut, "Filename: "); |
|||
TextIO.flushOut TextIO.stdOut; |
|||
removeExtension (TextIO.inputLine TextIO.stdIn)) |
|||
|
|||
|
|||
fun compile jobname = |
|||
let |
|||
val theFile = Files.readFile jobname |
|||
val _ = println("Translating the model\n"); |
|||
val _ = Debugging.log "Starting semantic analysis" |
|||
val M = Semantic.analyse |
|||
(Parser.parse |
|||
(Lexer.analyse theFile)) |
|||
val _ = Debugging.log "Finished semantic analysis" |
|||
val _ = Debugging.log "Starting translation" |
|||
val prism_output = translate M jobname |
|||
val _ = Debugging.log "Finished translation" |
|||
in |
|||
prism_output |
|||
end |
|||
|
|||
|
|||
fun run jobname = |
|||
let |
|||
val prism_output = compile jobname |
|||
val prism_out = TextIO.openOut (jobname ^ "_pepa.sm") |
|||
in |
|||
println("Writing PRISM output to \"" ^ |
|||
jobname ^ "_pepa.sm\"\n"); |
|||
TextIO.output (prism_out, prism_output); |
|||
TextIO.closeOut prism_out |
|||
end |
|||
|
|||
|
|||
fun main args = |
|||
let |
|||
val _ = runningInteractively := args = [] |
|||
val otherArgs = CommandLine.arguments () |
|||
in |
|||
println("PEPA to PRISM compiler [version "^ |
|||
PEPA_version ^ ", " ^ |
|||
PEPA_compiled ^ "]\n"); |
|||
let val jobname = getJobName args |
|||
in |
|||
(* Check if debugging requested first *) |
|||
Debugging.checkRequested(); |
|||
Extractor.initialise jobname; |
|||
run jobname; |
|||
Extractor.finalise (); |
|||
println("Exiting PEPA to PRISM compiler.\n") |
|||
end |
|||
end |
|||
|
|||
end; |
|||
@ -1,10 +0,0 @@ |
|||
(* |
|||
File: Parser.sig |
|||
|
|||
Signature for the structure which contains the PEPA parser |
|||
*) |
|||
|
|||
signature Parser = |
|||
sig |
|||
val parse : Lexer.token list -> Pepa.Component |
|||
end; |
|||
@ -1,183 +0,0 @@ |
|||
(* |
|||
File: Parser.sml |
|||
|
|||
The structure which contains the PEPA parser |
|||
*) |
|||
|
|||
structure Parser |
|||
:> Parser |
|||
= struct |
|||
|
|||
(* Parser tools. Taken from Chris Reade's |
|||
book ``Elements of Functional Programming''. |
|||
*) |
|||
|
|||
(* Utility functions *) |
|||
|
|||
fun pair a b = (a,b) |
|||
fun fst(x,y) = x |
|||
fun snd(x,y) = y |
|||
|
|||
fun consonto x a = a :: x |
|||
fun fold f [] b = b |
|||
| fold f (h::t) b = f (h, fold f t b) |
|||
fun link llist = fold (op @) llist [] |
|||
|
|||
datatype 'a possible = |
|||
Ok of 'a |
|||
| Fail |
|||
|
|||
type 'a parser = Lexer.token list -> ('a * Lexer.token list) possible |
|||
|
|||
infixr 4 <&> |
|||
infixr 3 <|> |
|||
infix 0 modify |
|||
|
|||
fun (parser1 <|> parser2) s = |
|||
let fun parser2_if_fail Fail = parser2 s |
|||
| parser2_if_fail x = x |
|||
in |
|||
parser2_if_fail (parser1 s) |
|||
end |
|||
|
|||
fun (parser modify f) s = |
|||
let fun modresult Fail = Fail |
|||
| modresult (Ok (x, y)) = Ok (f x, y) |
|||
in |
|||
modresult (parser s) |
|||
end |
|||
|
|||
fun (parser1 <&> parser2) s = |
|||
let fun parser2_after Fail = Fail |
|||
| parser2_after (Ok (x1, s1)) = (parser2 modify (pair x1)) s1 |
|||
in |
|||
parser2_after (parser1 s) |
|||
end |
|||
|
|||
fun emptyseq s = Ok ([], s) |
|||
|
|||
fun optional pr = (pr modify (consonto [])) |
|||
<|> emptyseq |
|||
|
|||
fun sequence pr = |
|||
let fun seqpr s = ((pr <&> seqpr modify (op ::)) |
|||
<|> emptyseq) s |
|||
in |
|||
seqpr |
|||
end |
|||
|
|||
fun seqwith (front, sep, back) pr = |
|||
let val sep_pr = sep <&> pr modify snd |
|||
val items = pr <&> sequence sep_pr modify (op ::) |
|||
in |
|||
front <&> optional items <&> back modify (link o fst o snd) |
|||
end |
|||
|
|||
fun parserList [] = emptyseq |
|||
| parserList (pr :: rest) = pr <&> (parserList rest) modify (op ::) |
|||
|
|||
fun alternatives [] = (fn x => Fail) |
|||
| alternatives (pr :: rest) = pr <|> alternatives rest; |
|||
|
|||
|
|||
|
|||
(* Basic parsers *) |
|||
|
|||
fun variable (Lexer.Ident x :: s) = Ok (x, s) |
|||
| variable other = Fail |
|||
|
|||
fun float (Lexer.Float x :: s) = Ok (x, s) |
|||
| float other = Fail |
|||
|
|||
fun literal a (Lexer.Symbol x :: s) = if a = x then Ok (x, s) else Fail |
|||
| literal a other = Fail; |
|||
|
|||
|
|||
|
|||
(* A parser for PEPA. |
|||
*) |
|||
|
|||
|
|||
fun unparenth (bra, (e, ket)) = e; |
|||
|
|||
fun bracedseq s = seqwith (literal #"{", literal #",", literal #"}") s; |
|||
|
|||
fun angledseq s = seqwith (literal #"<", literal #",", literal #">") s; |
|||
|
|||
val actlist : Pepa.Identifier list parser = bracedseq variable; |
|||
|
|||
val cooplist: Pepa.Identifier list parser = angledseq variable; |
|||
|
|||
fun def s = ((adef <&> optional (literal #";" <&> def) modify opt_consts) |
|||
<|> agenta ) s |
|||
|
|||
and adef s = (optional (literal #"#") <&> variable <&> |
|||
literal #"=" <&> agentd modify mk_const) s |
|||
|
|||
and agenta s = (agentb <&> optional (literal #"/" <&> actlist) |
|||
modify mk_hiding) s |
|||
|
|||
and agentb s = (agentc <&> optional (literal #"+" <&> agentb) |
|||
modify mk_plus) s |
|||
|
|||
and agentc s = (agent <&> optional (cooplist <&> agentc) |
|||
modify mk_coop) s |
|||
|
|||
and agentd s = (agent <&> optional (literal #"+" <&> agentd) |
|||
modify mk_plus) s |
|||
|
|||
and agent s = ((literal #"(" <&> variable <&> |
|||
literal #"," <&> variable <&> |
|||
literal #")" <&> literal #"." <&> |
|||
agent modify mk_prefix) |
|||
<|> (literal #"(" <&> agenta <&> literal #")" |
|||
modify unparenth) |
|||
<|> (variable modify mk_agent) |
|||
<|> (float modify mk_rate)) s |
|||
|
|||
and mk_agent s = Pepa.VAR s |
|||
|
|||
and mk_rate s = Pepa.RATE s |
|||
|
|||
and mk_const (hash, (i, (eq, e))) = (i, e) |
|||
|
|||
and mk_hiding (P, []) = P |
|||
| mk_hiding (P, [(slash, L)]) = Pepa.HIDING (P, L) |
|||
| mk_hiding other = error "hiding" |
|||
|
|||
and mk_plus (P, []) = P |
|||
| mk_plus (P, [(plus, Q)]) = Pepa.CHOICE (P, Q) |
|||
| mk_plus other = error "plus" |
|||
|
|||
and mk_coop (P, []) = P |
|||
| mk_coop (P, [(L, Q)]) = Pepa.COOP (P, Q, L) |
|||
| mk_coop other = error "cooperation" |
|||
|
|||
and mk_prefix (bra, (alpha, (comma, (rate, (ket, (dot, P)))))) |
|||
= Pepa.PREFIX ((alpha, rate), P) |
|||
|
|||
and opt_consts ((i, e1), [(oper, e2)]) = Pepa.CONSTS (i, e1, e2) |
|||
| opt_consts ((i, e1), _) = error ("constants: at or near " ^ i) |
|||
|
|||
and error s = Error.parse_error s |
|||
|
|||
local |
|||
fun lit (Lexer.Symbol #";") = ";\n" |
|||
| lit (Lexer.Symbol #"=") = " = " |
|||
| lit (Lexer.Symbol #"+") = " + " |
|||
| lit (Lexer.Symbol #",") = ", " |
|||
| lit (Lexer.Symbol #"<") = " <" |
|||
| lit (Lexer.Symbol #">") = "> " |
|||
| lit (Lexer.Symbol c) = str c |
|||
| lit (Lexer.Float s) = s |
|||
| lit (Lexer.Ident s) = s |
|||
in |
|||
fun report Fail = error "ill-formed PEPA model definition" |
|||
| report (Ok (c, [])) = c |
|||
| report (Ok (c, x)) = error (String.concat |
|||
("Unparsed :-\n" :: (map lit x))) |
|||
end |
|||
|
|||
val parse = report o def |
|||
|
|||
end; |
|||
@ -1,33 +0,0 @@ |
|||
(* |
|||
File: Pepa.sig |
|||
|
|||
Interface to the internals of the PEPA Workbench. |
|||
*) |
|||
|
|||
signature Pepa = |
|||
sig |
|||
type Identifier = string |
|||
|
|||
type Name = int |
|||
|
|||
datatype Component = |
|||
PREFIX of (Identifier * Identifier) * Component |
|||
| CHOICE of Component * Component |
|||
| COOP of Component * Component * Identifier list |
|||
| HIDING of Component * Identifier list |
|||
| VAR of Identifier |
|||
| RATE of string |
|||
| CONSTS of Identifier * Component * Component |
|||
|
|||
(* States and components are isomorphic. The difference |
|||
is that components are specified by the modeller and |
|||
states are found by the Workbench. |
|||
*) |
|||
type State = Component |
|||
|
|||
type Environment = (Identifier * Component) list |
|||
|
|||
type Transition = Component * |
|||
((Identifier * Identifier) * Name) option * Component |
|||
|
|||
end; |
|||
@ -1,54 +0,0 @@ |
|||
(* |
|||
File: Pepa.sml |
|||
|
|||
Datatypes of the PEPA Workbench. |
|||
*) |
|||
|
|||
structure Pepa |
|||
:> Pepa |
|||
= struct |
|||
type Identifier = string |
|||
|
|||
type Name = int |
|||
|
|||
datatype Component = |
|||
PREFIX of (Identifier * Identifier) * Component |
|||
| CHOICE of Component * Component |
|||
| COOP of Component * Component * Identifier list |
|||
| HIDING of Component * Identifier list |
|||
| VAR of Identifier |
|||
| RATE of string |
|||
| CONSTS of Identifier * Component * Component |
|||
|
|||
type State = Component |
|||
|
|||
type Environment = (Identifier * Component) list |
|||
|
|||
type Transition = Component * |
|||
((Identifier * Identifier) * Name) option * Component |
|||
|
|||
|
|||
(* |
|||
Identifiers and Names |
|||
===================== |
|||
An identifier is an alphanumeric descriptor assigned by the PEPA modeller |
|||
whereas a name is a numeric stamp computed by the PEPA Workbench to allow |
|||
the workbench to distinguish between repeated occurrences of a component. |
|||
Names are assigned by the `derivative' function on traversing the tree |
|||
of the abstract syntax of the PEPA model. Names are assigned thus: |
|||
|
|||
0 |
|||
/ \ |
|||
1 2 |
|||
/ \ / \ |
|||
3 4 5 6 |
|||
|
|||
doubling as we go down the tree and adding 1 if we go left and 2 if we go |
|||
right. This will make a distinction between P <> P <> P <> P, numbering the |
|||
copies 1, 5, 13 and 14 and a bushier tree, (P <> P) <> (P <> P), numbering |
|||
these copies 3, 4, 5, 6. In either case the effect is the same: to have |
|||
unique numbers for the leaves of the tree (the sequential components) and |
|||
the nodes (the cooperations). |
|||
*) |
|||
|
|||
end; |
|||
@ -1,12 +0,0 @@ |
|||
(* |
|||
File: Prettyprinter.sig |
|||
|
|||
Signature for the structure which prettyprints PEPA models |
|||
*) |
|||
|
|||
signature Prettyprinter = |
|||
sig |
|||
datatype printmode = compressed | uncompressed | verbose | asPRISM |
|||
val print : printmode -> Pepa.Component -> string |
|||
val printtransition : printmode -> Pepa.Transition -> string |
|||
end; |
|||
@ -1,88 +0,0 @@ |
|||
(* |
|||
File: Prettyprinter.sml |
|||
|
|||
The structure which prettyprints PEPA models |
|||
*) |
|||
|
|||
structure Prettyprinter |
|||
:> Prettyprinter |
|||
= struct |
|||
|
|||
datatype printmode = compressed | uncompressed | verbose | asPRISM |
|||
|
|||
fun print mode = |
|||
let |
|||
fun pp (Pepa.PREFIX ((alpha, rate), P)) |
|||
= "("^printid alpha^", "^printid rate^")."^(pp P) |
|||
| pp (Pepa.CHOICE (P, Q)) |
|||
= (pp P) ^ " + " ^ (pp Q) |
|||
| pp (Pepa.COOP (P, Q, L)) |
|||
= (pp P) |
|||
^ (if mode = verbose then " <" ^ (printlist L) ^ "> " else "|") |
|||
^ (pp Q) |
|||
| pp (Pepa.HIDING (P, [])) |
|||
= (pp P) |
|||
| pp (Pepa.HIDING (P, L)) |
|||
= (pp P) ^ "/{" ^ (printlist L) ^ "}" |
|||
| pp (Pepa.VAR I) |
|||
= printid I |
|||
| pp (Pepa.RATE r) = r |
|||
| pp (Pepa.CONSTS (I, P, L)) |
|||
= printid I ^ " = " ^ (pp P) ^ ";\n" ^ (pp L) |
|||
and printid s = s |
|||
and printlist nil = "" |
|||
| printlist [x] = printid x |
|||
| printlist (x::y::z) = printid x ^ ", " ^ (printlist (y::z)) |
|||
local |
|||
val l : string list ref = ref [] |
|||
fun countList I [] = 0 |
|||
| countList I (h::t) = (if I = h then 1 else 0) + countList I t |
|||
in |
|||
fun count I = (l := I :: !l; countList I (!l)) |
|||
end |
|||
fun p2p (Pepa.COOP (P, Q, [])) |
|||
= "(" |
|||
^ (p2p P) |
|||
^ (" ||| ") |
|||
^ (p2p Q) |
|||
^ ")" |
|||
| p2p (Pepa.COOP (P, Q, L)) |
|||
= "(" |
|||
^ (p2p P) |
|||
^ (" |[" ^ (printlist L) ^ "]| ") |
|||
^ (p2p Q) |
|||
^ ")" |
|||
| p2p (Pepa.HIDING (P, [])) |
|||
= "(" |
|||
^ (p2p P) |
|||
^ ")" |
|||
| p2p (Pepa.HIDING (P, L)) |
|||
= "(" |
|||
^ (p2p P) ^ "/{" ^ (printlist L) ^ "}" |
|||
^ ")" |
|||
| p2p (Pepa.VAR I) |
|||
= (case count I of |
|||
1 => printid I |
|||
| n => printid I ^ "_" ^ Int.toString n) |
|||
| p2p (Pepa.CONSTS (I, P, L)) |
|||
= p2p L |
|||
| p2p _ = "" |
|||
and printid s = s |
|||
and printlist nil = "" |
|||
| printlist [x] = printid x |
|||
| printlist (x::y::z) = printid x ^ ", " ^ (printlist (y::z)) |
|||
in if mode = asPRISM then p2p else pp |
|||
end |
|||
|
|||
fun printtransition mode (P, NONE ,Q) = |
|||
(* Note: phantom transition introduced ?? *) |
|||
(print mode P) ^ |
|||
"~~~>" ^ |
|||
(print mode Q) ^ "\n" |
|||
| printtransition mode (P, SOME ((a, r), n), Q) = |
|||
(print mode P) ^ |
|||
"~~" ^ a ^ "," ^ |
|||
r ^ "," ^Int.toString n ^ "~>" ^ |
|||
(print mode Q) ^ "\n" |
|||
|
|||
end; |
|||
@ -1,59 +0,0 @@ |
|||
|
|||
PEPA to PRISM Compiler Release 0.03.2 |
|||
===================================== |
|||
|
|||
This is the source code of release 0.03.2 of the PEPA to PRISM |
|||
Compiler. This software is distributed under the GNU Public License. |
|||
Please see the file COPYING in this directory for details. |
|||
|
|||
The PEPA to PRISM Compiler includes both Standard ML and Java source |
|||
code. To recompile the compile from source requires MLj 0.1 and a |
|||
Java compiler. The Java source code has been compiled with SUN's |
|||
J2SDK version 1.3.0 and 1.4.1-b21 but earlier or later releases should |
|||
also be able to compile these Java classes. The Java reflection API |
|||
is used so it must be available with your Java compiler. |
|||
|
|||
To recompile,type: |
|||
|
|||
(make; cd JAVA; make) |
|||
|
|||
Please contact Stephen Gilmore (Stephen.Gilmore@ed.ac.uk) if you have |
|||
difficulty in compiling or using the PEPA to PRISM Compiler. However, |
|||
please note that it is supplied without any warranty. The latest |
|||
release of any of the PEPA modelling tools can always be obtained from |
|||
the WWW page http://www.dcs.ed.ac.uk/pepa |
|||
|
|||
|
|||
Stephen Gilmore |
|||
Laboratory for Foundations of Computer Science |
|||
The University of Edinburgh |
|||
Monday 2nd December 2002 |
|||
|
|||
|
|||
Using the compiler |
|||
================== |
|||
|
|||
To run the compiler on a small input file type |
|||
|
|||
java -cp JAVA:pepa.zip pepa.compiler.Main TESTS/small.pepa |
|||
|
|||
where the contents of the file TESTS/small.pepa are |
|||
|
|||
r = 1.0; |
|||
t = 1.56; |
|||
|
|||
P = (a, r).P2; |
|||
P2 = (b, t).P; |
|||
|
|||
P <> P |
|||
|
|||
If you would like to know how the input PEPA components are mapped to |
|||
PRISM MTBDD variables you can request the compiler to record |
|||
information about this extraction process by creating a file named |
|||
".pepa_compiler_log_true" in the current working directory. The file |
|||
may be empty. |
|||
|
|||
To get verbose diagnostic information about the compilation process |
|||
create a file called ".pepa_compiler_debug_true" in the current |
|||
working directory. The file may be empty. |
|||
|
|||
@ -1,22 +0,0 @@ |
|||
--------------------------------------------------------------------- |
|||
PLEASE NOTE: |
|||
--------------------------------------------------------------------- |
|||
|
|||
This distribution of the PEPA to PRISM Compiler contains a minor |
|||
modification which will (presumably) need to be reversed to get it |
|||
to compile from source: |
|||
|
|||
* the file pepa.sml has been renamed to pepa.renamed.sml |
|||
|
|||
At present, the version distributed with PRISM is precompiled so this |
|||
should only be an issue if you want to recompile the package from source. |
|||
|
|||
For info, this change is in order to allow compilation of PRISM under |
|||
Windows and, more generally, to allow unpacking of the PRISM distribution |
|||
with tools such as WinZip. Windows/WinZip do not treat filenames in a |
|||
case-sensitive fashion; hence Pepa.sml/pepa.sml are indistinguishable. |
|||
|
|||
--------------------------------------------------------------------- |
|||
|
|||
Dave Parker |
|||
12/07/2004 |
|||
@ -1,12 +0,0 @@ |
|||
(* |
|||
File: Semantic.sig |
|||
|
|||
Signature for the structure which performs semantic analysis of |
|||
PEPA models |
|||
|
|||
*) |
|||
|
|||
signature Semantic = |
|||
sig |
|||
val analyse : Pepa.Component -> Pepa.Component |
|||
end; |
|||
@ -1,154 +0,0 @@ |
|||
(* |
|||
File: Semantic.sml |
|||
|
|||
The structure which performs semantic analysis of PEPA models. |
|||
Errors include component definitions which are missing or duplicated. |
|||
Warnings include components which are defined but never used and |
|||
occurrences of taus or wholly unused activity identifiers in any set |
|||
(hiding or cooperation). |
|||
|
|||
*) |
|||
|
|||
|
|||
structure Semantic |
|||
:> Semantic |
|||
= struct |
|||
|
|||
local |
|||
fun act (Pepa.PREFIX ((a, _), C)) = a :: act C |
|||
| act (Pepa.VAR _) = [] |
|||
| act (Pepa.RATE _) = [] |
|||
| act (Pepa.CHOICE (P, Q)) = act P @ act Q |
|||
| act (Pepa.COOP (P, Q, _)) = act P @ act Q |
|||
| act (Pepa.HIDING (P, _)) = act P |
|||
| act (Pepa.CONSTS (_, P, C)) = act P @ act C |
|||
|
|||
fun rates (Pepa.PREFIX ((_, r), C)) = r :: rates C |
|||
| rates (Pepa.VAR _) = [] |
|||
| rates (Pepa.RATE r) = [] (* this is a definition, not a use *) |
|||
| rates (Pepa.CHOICE (P, Q)) = rates P @ rates Q |
|||
| rates (Pepa.COOP (P, Q, _)) = rates P @ rates Q |
|||
| rates (Pepa.HIDING (P, _)) = rates P |
|||
| rates (Pepa.CONSTS (_, P, C)) = rates P @ rates C |
|||
|
|||
fun used (Pepa.VAR I) = [I] |
|||
| used (Pepa.RATE _) = [] |
|||
| used (Pepa.PREFIX (_, C)) = used C |
|||
| used (Pepa.CHOICE (P, Q)) = used P @ used Q |
|||
| used (Pepa.COOP (P, Q, _)) = used P @ used Q |
|||
| used (Pepa.HIDING (P, _)) = used P |
|||
| used (Pepa.CONSTS (_, P, C)) = used P @ used C |
|||
|
|||
fun defined (Pepa.CONSTS (I, Pepa.RATE _, C)) = defined C |
|||
| defined (Pepa.CONSTS (I, _, C)) = I :: defined C |
|||
| defined _ = [] |
|||
|
|||
fun ratesDefined (Pepa.CONSTS (I, Pepa.RATE _, C)) = I :: ratesDefined C |
|||
| ratesDefined _ = [] |
|||
in |
|||
val activities = Sort.quicksort o act |
|||
val used = Sort.quicksort o used |
|||
val ratesUsed = Sort.quicksort o rates |
|||
val defined = Sort.quicksort o defined |
|||
val ratesDefined = Sort.quicksort o ratesDefined |
|||
end |
|||
|
|||
fun rmDup [] = [] |
|||
| rmDup [x] = ([x] : string list) |
|||
| rmDup (x1 :: (t as (x2 :: _))) = |
|||
let val tail = rmDup t |
|||
in if x1 = x2 then tail else x1 :: tail |
|||
end |
|||
|
|||
local |
|||
fun fstNotSnd ([], _) = [] |
|||
| fstNotSnd (fst, []) = (fst : string list) |
|||
| fstNotSnd (h1::fst, h2::snd) = |
|||
if h1 < h2 |
|||
then h1 :: fstNotSnd (fst, h2::snd) |
|||
else if h1 = h2 then fstNotSnd (fst, h2::snd) |
|||
else fstNotSnd (h1::fst, snd) |
|||
in |
|||
fun firstNotSecond (fst, snd) = fstNotSnd (rmDup fst, rmDup snd) |
|||
end |
|||
|
|||
fun checkDup s [] = () |
|||
| checkDup s [_] = () |
|||
| checkDup s (x1 :: (t as (x2 :: _))) = |
|||
if x1 = x2 |
|||
then |
|||
Error.fatal_error (s ^ " multiply defined: " ^ x1) |
|||
else checkDup s t |
|||
|
|||
fun reportNotUsed s C = |
|||
Error.warning (s ^ " definition unused: " ^ C) |
|||
|
|||
fun reportNotDefined s C = |
|||
Error.fatal_error (s ^ " not defined: " ^ C) |
|||
|
|||
(* Seems not to be the bug *) |
|||
(* This version of member works on sorted string lists *) |
|||
fun member (s : string) = |
|||
let |
|||
fun mem [] = false |
|||
| mem (h::t) = |
|||
not (h > s) andalso (h = s orelse mem t) |
|||
in mem end |
|||
|
|||
fun purifylist act class = |
|||
let |
|||
fun pL [] = [] |
|||
| pL (h :: t) = |
|||
case h of |
|||
"tau" => |
|||
(Error.warning ("tau found in " ^ class ^ " set, ignoring"); |
|||
pL t) |
|||
| id => |
|||
if member id act |
|||
then id :: pL t |
|||
else (Error.warning ("unused activity name `" ^ |
|||
id ^ "' found in " ^ class ^ " set, ignoring"); |
|||
pL t) |
|||
|
|||
in pL end |
|||
|
|||
fun purify act = |
|||
let |
|||
fun p (Pepa.COOP (P, Q, L)) = |
|||
Pepa.COOP (p P, p Q, purifylist act "cooperation" L) |
|||
| p (Pepa.HIDING (P, L)) = |
|||
Pepa.HIDING (p P, purifylist act "hiding" L) |
|||
| p (Pepa.CONSTS (I, P, C)) = |
|||
Pepa.CONSTS (I, p P, p C) |
|||
| p C = C |
|||
in p end |
|||
|
|||
fun analyse C = |
|||
let |
|||
val usedActivities = rmDup (activities C) |
|||
val usedNames = used C |
|||
val definedNames = defined C |
|||
val defNotUsed = firstNotSecond (definedNames, usedNames) |
|||
val _ = map (reportNotUsed "Component") defNotUsed |
|||
|
|||
val usedRates = ratesUsed C |
|||
val definedRates = ratesDefined C |
|||
val defNotUsedRates = firstNotSecond (definedRates, usedRates) |
|||
val _ = map (reportNotUsed "Rate") defNotUsedRates |
|||
|
|||
val usedNotDefined = firstNotSecond (usedNames, definedNames) |
|||
val _ = map (reportNotDefined "Component") usedNotDefined |
|||
val _ = checkDup "Component" definedNames |
|||
|
|||
val usedNotDefinedRates = |
|||
firstNotSecond (usedRates, Sort.quicksort ("infty" :: definedRates)) |
|||
(* infty is predefined *) |
|||
|
|||
val _ = map (reportNotDefined "Rate") usedNotDefinedRates |
|||
val _ = checkDup "Rate" definedRates |
|||
|
|||
in |
|||
purify usedActivities C |
|||
end |
|||
|
|||
end; |
|||
@ -1,11 +0,0 @@ |
|||
(* |
|||
File: Sort.sig |
|||
|
|||
Signature for the structure which contains utility functions |
|||
for sorting string lists. |
|||
*) |
|||
|
|||
signature Sort = |
|||
sig |
|||
val quicksort : string list -> string list |
|||
end; |
|||
@ -1,24 +0,0 @@ |
|||
(* |
|||
File: Sort.sml |
|||
|
|||
Utility structure for sorting string lists. |
|||
*) |
|||
|
|||
structure Sort |
|||
:> Sort |
|||
= struct |
|||
|
|||
fun quicksort ([] : string list) = [] |
|||
| quicksort [x] = [x] |
|||
| quicksort (a::rest) = (* the head "a" is the pivot *) |
|||
let |
|||
fun split(left,right,[]) = quicksort left @ (a::quicksort right) |
|||
| split(left,right,x::l) = |
|||
if x <= a |
|||
then split(x::left,right,l) |
|||
else split(left,x::right,l) |
|||
in |
|||
split([],[],rest) |
|||
end |
|||
|
|||
end; |
|||
@ -1,8 +0,0 @@ |
|||
|
|||
The files in this directory should be rejected by the PEPA compiler |
|||
because they contain deliberate errors. Thus there is no |
|||
corresponding output for these input PEPA models. |
|||
|
|||
Stephen Gilmore <stg@inf.ed.ac.uk> |
|||
2-12-2002 |
|||
|
|||
@ -1,7 +0,0 @@ |
|||
r = 1.0; |
|||
s = 2.0; |
|||
|
|||
P = (a,r).P; |
|||
Q = (a,s).Q; |
|||
|
|||
P <a> Q |
|||
@ -1,4 +0,0 @@ |
|||
|
|||
P = (a,r).P; |
|||
|
|||
P <> P |
|||
@ -1,7 +0,0 @@ |
|||
|
|||
The files in this directory are valid PEPA inputs to the PEPA-to-PRISM |
|||
compiler and have corresponding output files. |
|||
|
|||
Stephen Gilmore <stg@inf.ed.ac.uk> |
|||
2-12-2002 |
|||
|
|||
@ -1,110 +0,0 @@ |
|||
|
|||
%%% The Auction model by Hillston and Kloul |
|||
%%% as published in the paper Concurrency: Practice and Experience |
|||
|
|||
su=9.0; |
|||
sd=9.0; |
|||
st=2.0; |
|||
s=1.0; |
|||
pr=1.2; |
|||
ppr=0.8; |
|||
qr=1.2; |
|||
qqr=0.8; |
|||
r=2.0; |
|||
|
|||
Bidder = (bid_in,su).WaitingBid + (preq_in, sd).WaitingPrice; |
|||
WaitingBid = (forward_accept, T).Bidder + (forward_reject, T).Incorrect; |
|||
WaitingPrice = (forward_presp,T).Bidder; |
|||
Incorrect = (preq_in, st).WaitingPrice; |
|||
|
|||
|
|||
Bidder_CN = (bid'_in,su).WaitingBid_CN + (preq'_in, sd).WaitingPrice_CN; |
|||
WaitingBid_CN = (forward_accept', T).Bidder_CN |
|||
+ (forward_reject', T).Incorrect_CN; |
|||
WaitingPrice_CN = (forward_presp',T).Bidder_CN; |
|||
Incorrect_CN = (preq'_in, st).WaitingPrice_CN; |
|||
|
|||
|
|||
Node = (bid_in, T).Node1 + (preq_in, T).Node2 |
|||
+ (accept_s, T).Node3 |
|||
+ (reject_s, T).Node4 |
|||
+ (presp_s, T).Node5; |
|||
Node1 = (forward_bid, s).Node |
|||
+ (presp_s, T).Node6 |
|||
+ (accept_s, T).Node7 |
|||
+ (reject_s, T).Node8; |
|||
Node2 = (forward_preq, s).Node |
|||
+ (presp_s, T).Node9 |
|||
+ (accept_s, T).Node10 |
|||
+ (reject_s, T).Node11; |
|||
Node3 =(forward_accept, s).Node; |
|||
Node4 =(forward_reject, s).Node; |
|||
Node5 =(forward_presp, s).Node; |
|||
Node6 =(forward_presp, s).Node1; |
|||
Node7 =(forward_accept, s).Node1; |
|||
Node8 =(forward_reject, s).Node1; |
|||
Node9 =(forward_presp, s).Node2; |
|||
Node10 =(forward_accept, s).Node2; |
|||
Node11 =(forward_reject, s).Node2; |
|||
|
|||
CNode = (bid'_in,T).CNode1 + (preq'_in,T).CNode2 |
|||
+ (forward_accept_sc,T).CNode3 |
|||
+ (forward_reject_sc,T).CNode4 |
|||
+ (forward_presp_sc, T).CNode5; |
|||
CNode1 = (forward_bid_nc, s).CNode |
|||
+ (forward_accept_sc,T).CNode6 |
|||
+ (forward_reject_sc,T).CNode7 |
|||
+ (forward_presp_sc, T).CNode8; |
|||
CNode2 = (forward_preq_nc, s).CNode |
|||
+ (forward_accept_sc,T).CNode9 |
|||
+ (forward_reject_sc,T).CNode10 |
|||
+ (forward_presp_sc, T).CNode11; |
|||
CNode3 = (forward_accept', s).CNode; |
|||
CNode4 =(forward_reject', s).CNode; |
|||
CNode5 =(forward_presp', s).CNode; |
|||
CNode6 =(forward_accept', s).CNode1; |
|||
CNode7 =(forward_reject', s).CNode1; |
|||
CNode8 =(forward_presp', s).CNode1; |
|||
CNode9 =(forward_accept', s).CNode2; |
|||
CNode10 =(forward_reject', s).CNode2; |
|||
CNode11 =(forward_presp', s).CNode2; |
|||
|
|||
|
|||
TNode = (bid_in, T).TNode1 + (forward_bid_nc, T).TNode1 |
|||
+ (preq_in, T).TNode2 + (forward_preq_nc, T).TNode2 |
|||
+ (accept_sc, T).TNode3 + (reject_sc, T).TNode4 |
|||
+ (presp_sc,T).TNode5; |
|||
TNode1 = (forward_bid_cs, s).TNode |
|||
+ (presp_sc,T).TNode6 |
|||
+ (accept_sc, T).TNode7 |
|||
+ (reject_sc, T).TNode8; |
|||
TNode2 = (forward_preq_cs, s).TNode |
|||
+ (presp_sc,T).TNode9 |
|||
+ (accept_sc, T).TNode10 |
|||
+ (reject_sc, T).TNode11; |
|||
TNode3 = (forward_accept_sc,s).TNode + (forward_accept, s).TNode; |
|||
TNode4 = (forward_reject_sc,s).TNode + (forward_reject, s).TNode; |
|||
TNode5 = (forward_presp_sc,s).TNode + (forward_presp, s).TNode; |
|||
TNode6 = (forward_presp_sc,s).TNode1 + (forward_presp, s).TNode1; |
|||
TNode7 = (forward_accept_sc,s).TNode1+ (forward_accept, s).TNode1; |
|||
TNode8 = (forward_reject_sc,s).TNode1+ (forward_reject, s).TNode1; |
|||
TNode9 = (forward_presp_sc,s).TNode2 + (forward_presp, s).TNode2; |
|||
TNode10= (forward_accept_sc,s).TNode2 + (forward_accept, s).TNode2; |
|||
TNode11= (forward_reject_sc,s).TNode2+ (forward_reject, s).TNode2; |
|||
|
|||
Server = (forward_bid,T).Server' + (forward_bid_cs,T).Server'' |
|||
+ (forward_preq,T).Server1 + (forward_preq_cs, T).Server2; |
|||
Server' = (accept_s,pr).Server + (reject_s,ppr).Server; |
|||
Server''= (accept_sc,qr).Server + (reject_sc,qqr).Server; |
|||
Server1 = (presp_s,r).Server; |
|||
Server2 = (presp_sc,r).Server; |
|||
|
|||
|
|||
((Server <accept_sc,reject_sc,presp_sc,forward_bid_cs,forward_preq_cs> |
|||
((Bidder <> Bidder) |
|||
<bid_in,forward_accept,forward_reject,preq_in,forward_presp> TNode)) |
|||
<forward_bid_nc,forward_accept_sc,forward_reject_sc,forward_preq_nc, |
|||
forward_presp_sc> (CNode <bid'_in,preq'_in,forward_accept',forward_reject', |
|||
forward_presp'> (Bidder_CN <> Bidder_CN))) |
|||
<accept_s,reject_s,presp_s,forward_preq,forward_bid> Node <bid_in,preq_in, forward_accept,forward_reject,forward_presp> |
|||
(Bidder <> Bidder) |
|||
@ -1,288 +0,0 @@ |
|||
// Output from the PEPA-to-PRISM compiler |
|||
// Version 0.03.1 "Balerno" |
|||
// Released: 24-10-2002 |
|||
// |
|||
// Model file: TESTS/auction |
|||
|
|||
// All PEPA models define CTMCs so mark this as a stochastic model |
|||
stochastic |
|||
|
|||
// The rates used in the model |
|||
rate su = 9.0; |
|||
rate sd = 9.0; |
|||
rate st = 2.0; |
|||
rate s = 1.0; |
|||
rate pr = 1.2; |
|||
rate ppr = 0.8; |
|||
rate qr = 1.2; |
|||
rate qqr = 0.8; |
|||
rate r = 2.0; |
|||
|
|||
|
|||
// Information about components inferred by the compiler |
|||
// during static analysis: |
|||
// |
|||
// interface CNode |
|||
// activity forward_accept' |
|||
// activity forward_bid_nc |
|||
// activity forward_preq_nc |
|||
// activity forward_presp' |
|||
// activity forward_reject' |
|||
// endinterface |
|||
// interface Node |
|||
// activity forward_accept |
|||
// activity forward_bid |
|||
// activity forward_preq |
|||
// activity forward_presp |
|||
// activity forward_reject |
|||
// endinterface |
|||
// interface Server |
|||
// activity accept_s |
|||
// activity accept_sc |
|||
// activity presp_s |
|||
// activity presp_sc |
|||
// activity reject_s |
|||
// activity reject_sc |
|||
// endinterface |
|||
// interface TNode |
|||
// activity forward_accept |
|||
// activity forward_accept_sc |
|||
// activity forward_bid_cs |
|||
// activity forward_preq_cs |
|||
// activity forward_presp |
|||
// activity forward_presp_sc |
|||
// activity forward_reject |
|||
// activity forward_reject_sc |
|||
// endinterface |
|||
|
|||
// interface Bidder |
|||
// activity bid_in |
|||
// activity preq_in |
|||
// endinterface |
|||
// interface Bidder_CN |
|||
// activity bid'_in |
|||
// activity preq'_in |
|||
// endinterface |
|||
|
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const Server = 0; |
|||
const Server' = 1; |
|||
const Server'' = 2; |
|||
const Server1 = 3; |
|||
const Server2 = 4; |
|||
module Server |
|||
|
|||
Server_STATE : [0..4] init Server; |
|||
|
|||
[forward_bid] (Server_STATE=Server) -> 1 : (Server_STATE'=Server'); |
|||
[forward_bid_cs] (Server_STATE=Server) -> 1 : (Server_STATE'=Server''); |
|||
[forward_preq] (Server_STATE=Server) -> 1 : (Server_STATE'=Server1); |
|||
[forward_preq_cs] (Server_STATE=Server) -> 1 : (Server_STATE'=Server2); |
|||
[accept_s] (Server_STATE=Server') -> pr : (Server_STATE'=Server); |
|||
[reject_s] (Server_STATE=Server') -> ppr : (Server_STATE'=Server); |
|||
[accept_sc] (Server_STATE=Server'') -> qr : (Server_STATE'=Server); |
|||
[reject_sc] (Server_STATE=Server'') -> qqr : (Server_STATE'=Server); |
|||
[presp_s] (Server_STATE=Server1) -> r : (Server_STATE'=Server); |
|||
[presp_sc] (Server_STATE=Server2) -> r : (Server_STATE'=Server); |
|||
|
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const Bidder = 0; |
|||
const WaitingBid = 1; |
|||
const WaitingPrice = 2; |
|||
module Bidder |
|||
|
|||
Bidder_STATE : [0..2] init Bidder; |
|||
|
|||
[bid_in] (Bidder_STATE=Bidder) -> su : (Bidder_STATE'=WaitingBid); |
|||
[preq_in] (Bidder_STATE=Bidder) -> sd : (Bidder_STATE'=WaitingPrice); |
|||
[forward_accept] (Bidder_STATE=WaitingBid) -> 1 : (Bidder_STATE'=Bidder); |
|||
[forward_reject] (Bidder_STATE=WaitingBid) -> 1 : (Bidder_STATE'=Incorrect); |
|||
[forward_presp] (Bidder_STATE=WaitingPrice) -> 1 : (Bidder_STATE'=Bidder); |
|||
|
|||
endmodule |
|||
|
|||
// We make another copy of module Bidder |
|||
module Bidder_2 = Bidder[Bidder_STATE=Bidder_2_STATE] |
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const TNode = 0; |
|||
const TNode1 = 1; |
|||
const TNode10 = 2; |
|||
const TNode11 = 3; |
|||
const TNode2 = 4; |
|||
const TNode3 = 5; |
|||
const TNode4 = 6; |
|||
const TNode5 = 7; |
|||
const TNode6 = 8; |
|||
const TNode7 = 9; |
|||
const TNode8 = 10; |
|||
const TNode9 = 11; |
|||
module TNode |
|||
|
|||
TNode_STATE : [0..11] init TNode; |
|||
|
|||
[bid_in] (TNode_STATE=TNode) -> 1 : (TNode_STATE'=TNode1); |
|||
[forward_bid_nc] (TNode_STATE=TNode) -> 1 : (TNode_STATE'=TNode1); |
|||
[preq_in] (TNode_STATE=TNode) -> 1 : (TNode_STATE'=TNode2); |
|||
[forward_preq_nc] (TNode_STATE=TNode) -> 1 : (TNode_STATE'=TNode2); |
|||
[accept_sc] (TNode_STATE=TNode) -> 1 : (TNode_STATE'=TNode3); |
|||
[reject_sc] (TNode_STATE=TNode) -> 1 : (TNode_STATE'=TNode4); |
|||
[presp_sc] (TNode_STATE=TNode) -> 1 : (TNode_STATE'=TNode5); |
|||
[forward_bid_cs] (TNode_STATE=TNode1) -> s : (TNode_STATE'=TNode); |
|||
[presp_sc] (TNode_STATE=TNode1) -> 1 : (TNode_STATE'=TNode6); |
|||
[accept_sc] (TNode_STATE=TNode1) -> 1 : (TNode_STATE'=TNode7); |
|||
[reject_sc] (TNode_STATE=TNode1) -> 1 : (TNode_STATE'=TNode8); |
|||
[forward_accept_sc] (TNode_STATE=TNode10) -> s : (TNode_STATE'=TNode2); |
|||
[forward_accept] (TNode_STATE=TNode10) -> s : (TNode_STATE'=TNode2); |
|||
[forward_reject_sc] (TNode_STATE=TNode11) -> s : (TNode_STATE'=TNode2); |
|||
[forward_reject] (TNode_STATE=TNode11) -> s : (TNode_STATE'=TNode2); |
|||
[forward_preq_cs] (TNode_STATE=TNode2) -> s : (TNode_STATE'=TNode); |
|||
[presp_sc] (TNode_STATE=TNode2) -> 1 : (TNode_STATE'=TNode9); |
|||
[accept_sc] (TNode_STATE=TNode2) -> 1 : (TNode_STATE'=TNode10); |
|||
[reject_sc] (TNode_STATE=TNode2) -> 1 : (TNode_STATE'=TNode11); |
|||
[forward_accept_sc] (TNode_STATE=TNode3) -> s : (TNode_STATE'=TNode); |
|||
[forward_accept] (TNode_STATE=TNode3) -> s : (TNode_STATE'=TNode); |
|||
[forward_reject_sc] (TNode_STATE=TNode4) -> s : (TNode_STATE'=TNode); |
|||
[forward_reject] (TNode_STATE=TNode4) -> s : (TNode_STATE'=TNode); |
|||
[forward_presp_sc] (TNode_STATE=TNode5) -> s : (TNode_STATE'=TNode); |
|||
[forward_presp] (TNode_STATE=TNode5) -> s : (TNode_STATE'=TNode); |
|||
[forward_presp_sc] (TNode_STATE=TNode6) -> s : (TNode_STATE'=TNode1); |
|||
[forward_presp] (TNode_STATE=TNode6) -> s : (TNode_STATE'=TNode1); |
|||
[forward_accept_sc] (TNode_STATE=TNode7) -> s : (TNode_STATE'=TNode1); |
|||
[forward_accept] (TNode_STATE=TNode7) -> s : (TNode_STATE'=TNode1); |
|||
[forward_reject_sc] (TNode_STATE=TNode8) -> s : (TNode_STATE'=TNode1); |
|||
[forward_reject] (TNode_STATE=TNode8) -> s : (TNode_STATE'=TNode1); |
|||
[forward_presp_sc] (TNode_STATE=TNode9) -> s : (TNode_STATE'=TNode2); |
|||
[forward_presp] (TNode_STATE=TNode9) -> s : (TNode_STATE'=TNode2); |
|||
|
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const CNode = 0; |
|||
const CNode1 = 1; |
|||
const CNode10 = 2; |
|||
const CNode11 = 3; |
|||
const CNode2 = 4; |
|||
const CNode3 = 5; |
|||
const CNode4 = 6; |
|||
const CNode5 = 7; |
|||
const CNode6 = 8; |
|||
const CNode7 = 9; |
|||
const CNode8 = 10; |
|||
const CNode9 = 11; |
|||
module CNode |
|||
|
|||
CNode_STATE : [0..11] init CNode; |
|||
|
|||
[bid'_in] (CNode_STATE=CNode) -> 1 : (CNode_STATE'=CNode1); |
|||
[preq'_in] (CNode_STATE=CNode) -> 1 : (CNode_STATE'=CNode2); |
|||
[forward_accept_sc] (CNode_STATE=CNode) -> 1 : (CNode_STATE'=CNode3); |
|||
[forward_reject_sc] (CNode_STATE=CNode) -> 1 : (CNode_STATE'=CNode4); |
|||
[forward_presp_sc] (CNode_STATE=CNode) -> 1 : (CNode_STATE'=CNode5); |
|||
[forward_bid_nc] (CNode_STATE=CNode1) -> s : (CNode_STATE'=CNode); |
|||
[forward_accept_sc] (CNode_STATE=CNode1) -> 1 : (CNode_STATE'=CNode6); |
|||
[forward_reject_sc] (CNode_STATE=CNode1) -> 1 : (CNode_STATE'=CNode7); |
|||
[forward_presp_sc] (CNode_STATE=CNode1) -> 1 : (CNode_STATE'=CNode8); |
|||
[forward_reject'] (CNode_STATE=CNode10) -> s : (CNode_STATE'=CNode2); |
|||
[forward_presp'] (CNode_STATE=CNode11) -> s : (CNode_STATE'=CNode2); |
|||
[forward_preq_nc] (CNode_STATE=CNode2) -> s : (CNode_STATE'=CNode); |
|||
[forward_accept_sc] (CNode_STATE=CNode2) -> 1 : (CNode_STATE'=CNode9); |
|||
[forward_reject_sc] (CNode_STATE=CNode2) -> 1 : (CNode_STATE'=CNode10); |
|||
[forward_presp_sc] (CNode_STATE=CNode2) -> 1 : (CNode_STATE'=CNode11); |
|||
[forward_accept'] (CNode_STATE=CNode3) -> s : (CNode_STATE'=CNode); |
|||
[forward_reject'] (CNode_STATE=CNode4) -> s : (CNode_STATE'=CNode); |
|||
[forward_presp'] (CNode_STATE=CNode5) -> s : (CNode_STATE'=CNode); |
|||
[forward_accept'] (CNode_STATE=CNode6) -> s : (CNode_STATE'=CNode1); |
|||
[forward_reject'] (CNode_STATE=CNode7) -> s : (CNode_STATE'=CNode1); |
|||
[forward_presp'] (CNode_STATE=CNode8) -> s : (CNode_STATE'=CNode1); |
|||
[forward_accept'] (CNode_STATE=CNode9) -> s : (CNode_STATE'=CNode2); |
|||
|
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const Bidder_CN = 0; |
|||
const WaitingBid_CN = 1; |
|||
const WaitingPrice_CN = 2; |
|||
module Bidder_CN |
|||
|
|||
Bidder_CN_STATE : [0..2] init Bidder_CN; |
|||
|
|||
[bid'_in] (Bidder_CN_STATE=Bidder_CN) -> su : (Bidder_CN_STATE'=WaitingBid_CN); |
|||
[preq'_in] (Bidder_CN_STATE=Bidder_CN) -> sd : (Bidder_CN_STATE'=WaitingPrice_CN); |
|||
[forward_accept'] (Bidder_CN_STATE=WaitingBid_CN) -> 1 : (Bidder_CN_STATE'=Bidder_CN); |
|||
[forward_reject'] (Bidder_CN_STATE=WaitingBid_CN) -> 1 : (Bidder_CN_STATE'=Incorrect_CN); |
|||
[forward_presp'] (Bidder_CN_STATE=WaitingPrice_CN) -> 1 : (Bidder_CN_STATE'=Bidder_CN); |
|||
|
|||
endmodule |
|||
|
|||
// We make another copy of module Bidder_CN |
|||
module Bidder_CN_2 = Bidder_CN[Bidder_CN_STATE=Bidder_CN_2_STATE] |
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const Node = 0; |
|||
const Node1 = 1; |
|||
const Node10 = 2; |
|||
const Node11 = 3; |
|||
const Node2 = 4; |
|||
const Node3 = 5; |
|||
const Node4 = 6; |
|||
const Node5 = 7; |
|||
const Node6 = 8; |
|||
const Node7 = 9; |
|||
const Node8 = 10; |
|||
const Node9 = 11; |
|||
module Node |
|||
|
|||
Node_STATE : [0..11] init Node; |
|||
|
|||
[bid_in] (Node_STATE=Node) -> 1 : (Node_STATE'=Node1); |
|||
[preq_in] (Node_STATE=Node) -> 1 : (Node_STATE'=Node2); |
|||
[accept_s] (Node_STATE=Node) -> 1 : (Node_STATE'=Node3); |
|||
[reject_s] (Node_STATE=Node) -> 1 : (Node_STATE'=Node4); |
|||
[presp_s] (Node_STATE=Node) -> 1 : (Node_STATE'=Node5); |
|||
[forward_bid] (Node_STATE=Node1) -> s : (Node_STATE'=Node); |
|||
[presp_s] (Node_STATE=Node1) -> 1 : (Node_STATE'=Node6); |
|||
[accept_s] (Node_STATE=Node1) -> 1 : (Node_STATE'=Node7); |
|||
[reject_s] (Node_STATE=Node1) -> 1 : (Node_STATE'=Node8); |
|||
[forward_accept] (Node_STATE=Node10) -> s : (Node_STATE'=Node2); |
|||
[forward_reject] (Node_STATE=Node11) -> s : (Node_STATE'=Node2); |
|||
[forward_preq] (Node_STATE=Node2) -> s : (Node_STATE'=Node); |
|||
[presp_s] (Node_STATE=Node2) -> 1 : (Node_STATE'=Node9); |
|||
[accept_s] (Node_STATE=Node2) -> 1 : (Node_STATE'=Node10); |
|||
[reject_s] (Node_STATE=Node2) -> 1 : (Node_STATE'=Node11); |
|||
[forward_accept] (Node_STATE=Node3) -> s : (Node_STATE'=Node); |
|||
[forward_reject] (Node_STATE=Node4) -> s : (Node_STATE'=Node); |
|||
[forward_presp] (Node_STATE=Node5) -> s : (Node_STATE'=Node); |
|||
[forward_presp] (Node_STATE=Node6) -> s : (Node_STATE'=Node1); |
|||
[forward_accept] (Node_STATE=Node7) -> s : (Node_STATE'=Node1); |
|||
[forward_reject] (Node_STATE=Node8) -> s : (Node_STATE'=Node1); |
|||
[forward_presp] (Node_STATE=Node9) -> s : (Node_STATE'=Node2); |
|||
|
|||
endmodule |
|||
|
|||
// We make another copy of module Bidder |
|||
module Bidder_3 = Bidder[Bidder_STATE=Bidder_3_STATE] |
|||
endmodule |
|||
|
|||
// We make another copy of module Bidder |
|||
module Bidder_4 = Bidder[Bidder_STATE=Bidder_4_STATE] |
|||
endmodule |
|||
|
|||
|
|||
// The system equation |
|||
system |
|||
(((Server |[accept_sc, reject_sc, presp_sc, forward_bid_cs, forward_preq_cs]| ((Bidder ||| Bidder_2) |[bid_in, forward_accept, forward_reject, preq_in, forward_presp]| TNode)) |[forward_bid_nc, forward_accept_sc, forward_reject_sc, forward_preq_nc, forward_presp_sc]| (CNode |[bid'_in, preq'_in, forward_accept', forward_reject', forward_presp']| (Bidder_CN ||| Bidder_CN_2))) |[accept_s, reject_s, presp_s, forward_preq, forward_bid]| (Node |[bid_in, preq_in, forward_accept, forward_reject, forward_presp]| (Bidder_3 ||| Bidder_4))) |
|||
endsystem |
|||
|
|||
// End of output from the PEPA-to-PRISM compiler |
|||
@ -1,22 +0,0 @@ |
|||
r = 2.0; |
|||
m = 2.0; |
|||
|
|||
# DB14 = (rep14,infty).DB14 + (rep15,infty).DB15 + (rep16,infty).DB16; |
|||
# DB15 = (rep14,infty).DB14 + (rep15,infty).DB15 + (rep16,infty).DB16; |
|||
# DB16 = (rep14,infty).DB14 + (rep15,infty).DB15 + (rep16,infty).DB16; |
|||
|
|||
# S14 = (reg14,infty).S14_prime; |
|||
# S14_prime = (rep14,r).S14; |
|||
|
|||
# S16 = (reg16,infty).S16_prime; |
|||
# S16_prime = (rep16,r).S16; |
|||
|
|||
# P14 = (reg14,r).P14 + (move15,m).P15; |
|||
# P15 = (move14,m).P14 + (reg15,r).P15 + (move16,m).P16; |
|||
# P16 = (move15,m).P15 + (reg16,r).P16; |
|||
|
|||
# S15 = (reg15,infty).S15_prime; |
|||
# S15_prime = (rep15,r).S15; |
|||
|
|||
|
|||
S15 <reg15,rep15> (S16 <reg16,rep16> ((S14 <rep14> DB14) <reg14> P14)) |
|||
@ -1,121 +0,0 @@ |
|||
// Output from the PEPA-to-PRISM compiler |
|||
// Version 0.03.2 "Jean Armour Avenue" |
|||
// Released: 08-11-2002 |
|||
// |
|||
// Model file: TESTS/badge.1.4 |
|||
|
|||
// All PEPA models define CTMCs so mark this as a stochastic model |
|||
stochastic |
|||
|
|||
// The rates used in the model |
|||
rate r = 2.0; |
|||
rate m = 2.0; |
|||
|
|||
|
|||
// Information about components inferred by the compiler |
|||
// during static analysis: |
|||
// |
|||
// interface DB14 empty: only individual or passive activities |
|||
// interface P14 |
|||
// activity reg14 |
|||
// activity reg15 |
|||
// activity reg16 |
|||
// endinterface |
|||
// interface S14 |
|||
// activity rep14 |
|||
// endinterface |
|||
// interface S15 |
|||
// activity rep15 |
|||
// endinterface |
|||
// interface S16 |
|||
// activity rep16 |
|||
// endinterface |
|||
|
|||
|
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const S15 = 0; |
|||
const S15_prime = 1; |
|||
module S15 |
|||
|
|||
S15_STATE : [0..1] init S15; |
|||
|
|||
[reg15] (S15_STATE=S15) -> 1 : (S15_STATE'=S15_prime); |
|||
[rep15] (S15_STATE=S15_prime) -> r : (S15_STATE'=S15); |
|||
|
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const S16 = 0; |
|||
const S16_prime = 1; |
|||
module S16 |
|||
|
|||
S16_STATE : [0..1] init S16; |
|||
|
|||
[reg16] (S16_STATE=S16) -> 1 : (S16_STATE'=S16_prime); |
|||
[rep16] (S16_STATE=S16_prime) -> r : (S16_STATE'=S16); |
|||
|
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const S14 = 0; |
|||
const S14_prime = 1; |
|||
module S14 |
|||
|
|||
S14_STATE : [0..1] init S14; |
|||
|
|||
[reg14] (S14_STATE=S14) -> 1 : (S14_STATE'=S14_prime); |
|||
[rep14] (S14_STATE=S14_prime) -> r : (S14_STATE'=S14); |
|||
|
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const DB14 = 0; |
|||
const DB15 = 1; |
|||
const DB16 = 2; |
|||
module DB14 |
|||
|
|||
DB14_STATE : [0..2] init DB14; |
|||
|
|||
[rep14] (DB14_STATE=DB14) -> 1 : (DB14_STATE'=DB14); |
|||
[rep15] (DB14_STATE=DB14) -> 1 : (DB14_STATE'=DB15); |
|||
[rep16] (DB14_STATE=DB14) -> 1 : (DB14_STATE'=DB16); |
|||
[rep14] (DB14_STATE=DB15) -> 1 : (DB14_STATE'=DB14); |
|||
[rep15] (DB14_STATE=DB15) -> 1 : (DB14_STATE'=DB15); |
|||
[rep16] (DB14_STATE=DB15) -> 1 : (DB14_STATE'=DB16); |
|||
[rep14] (DB14_STATE=DB16) -> 1 : (DB14_STATE'=DB14); |
|||
[rep15] (DB14_STATE=DB16) -> 1 : (DB14_STATE'=DB15); |
|||
[rep16] (DB14_STATE=DB16) -> 1 : (DB14_STATE'=DB16); |
|||
|
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const P14 = 0; |
|||
const P15 = 1; |
|||
const P16 = 2; |
|||
module P14 |
|||
|
|||
P14_STATE : [0..2] init P14; |
|||
|
|||
[reg14] (P14_STATE=P14) -> r : (P14_STATE'=P14); |
|||
[move15] (P14_STATE=P14) -> m : (P14_STATE'=P15); |
|||
[move14] (P14_STATE=P15) -> m : (P14_STATE'=P14); |
|||
[reg15] (P14_STATE=P15) -> r : (P14_STATE'=P15); |
|||
[move16] (P14_STATE=P15) -> m : (P14_STATE'=P16); |
|||
[move15] (P14_STATE=P16) -> m : (P14_STATE'=P15); |
|||
[reg16] (P14_STATE=P16) -> r : (P14_STATE'=P16); |
|||
|
|||
endmodule |
|||
|
|||
|
|||
// The system equation |
|||
system |
|||
(S15 |[reg15, rep15]| (S16 |[reg16, rep16]| ((S14 |[rep14]| DB14) |[reg14]| P14))) |
|||
endsystem |
|||
|
|||
// End of output from the PEPA-to-PRISM compiler |
|||
@ -1,6 +0,0 @@ |
|||
r = 1.0; |
|||
|
|||
P = (a,r).P'; |
|||
P' = (a,r).P; |
|||
|
|||
(P / {a}) <> P |
|||
@ -1,44 +0,0 @@ |
|||
// Output from the PEPA-to-PRISM compiler |
|||
// Version 0.03.1 "Balerno" |
|||
// Released: 24-10-2002 |
|||
// |
|||
// Model file: TESTS/hiding |
|||
|
|||
// All PEPA models define CTMCs so mark this as a stochastic model |
|||
stochastic |
|||
|
|||
// The rates used in the model |
|||
rate r = 1.0; |
|||
|
|||
|
|||
// Information about components inferred by the compiler |
|||
// during static analysis: |
|||
// |
|||
|
|||
// interface P empty: only individual or passive activities |
|||
|
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const P = 0; |
|||
const P' = 1; |
|||
module P |
|||
|
|||
P_STATE : [0..1] init P; |
|||
|
|||
[a] (P_STATE=P) -> r : (P_STATE'=P'); |
|||
[a] (P_STATE=P') -> r : (P_STATE'=P); |
|||
|
|||
endmodule |
|||
|
|||
// We make another copy of module P |
|||
module P_2 = P[P_STATE=P_2_STATE] |
|||
endmodule |
|||
|
|||
|
|||
// The system equation |
|||
system |
|||
((P/{a}) ||| P_2) |
|||
endsystem |
|||
|
|||
// End of output from the PEPA-to-PRISM compiler |
|||
@ -1,78 +0,0 @@ |
|||
% The Manhattan mobile phone model by Leila Kloul |
|||
|
|||
lambda1 = 0.5; |
|||
lambda2 = 1.8; |
|||
lambda3 = 1.0; |
|||
|
|||
mu = 0.008; |
|||
mu2 = 0.016; |
|||
mu3 = 0.024; |
|||
mu4 = 0.032; |
|||
mu5 = 0.040; |
|||
mu6 = 0.048; |
|||
mu7 = 0.054; |
|||
|
|||
alpha = 0.018; |
|||
alpha2 = 0.036; |
|||
alpha3 = 0.054; |
|||
alpha4 = 0.072; |
|||
alpha5 = 0.090; |
|||
alpha6 = 0.108; |
|||
alpha7 = 0.126; |
|||
|
|||
|
|||
|
|||
|
|||
#Macro0 = (in, lambda1).Macro1 + (handoff_up, top).Macro1 |
|||
+ (handoff_in_up_c, top).Macro1 + (handoff_out_up_c, top).Macro1; |
|||
#Macro1 = (in, lambda1).Macro2 + (handoff_up, top).Macro2 + (handoff_in_up_c, top).Macro2 |
|||
+ (handoff_out_up_c, top).Macro2 + (service, mu).Macro0; |
|||
#Macro2 = (in, lambda1).Macro3 + (handoff_up, top).Macro3 + (handoff_in_up_c, top).Macro3 |
|||
+ (handoff_out_up_c, top).Macro3 + (service, mu2).Macro1; |
|||
#Macro3 = (in, lambda1).Macro4 + (handoff_up, top).Macro4 + (handoff_in_up_c, top).Macro4 |
|||
+ (handoff_out_up_c, top).Macro4 + (service, mu3).Macro2; |
|||
#Macro4 = (in, lambda1).Macro5 + (handoff_up, top).Macro5 + (handoff_in_up_c, top).Macro5 |
|||
+ (handoff_out_up_c, top).Macro5 + (service, mu4).Macro3; |
|||
#Macro5 = (in, lambda1).Macro6 + (handoff_up, top).Macro6 + (handoff_in_up_c, top).Macro6 |
|||
+ (handoff_out_up_c, top).Macro6 + (service, mu5).Macro4; |
|||
#Macro6 = (in, lambda1).Macro7 + (handoff_up, top).Macro7 + (handoff_in_up_c, top).Macro7 |
|||
+ (handoff_out_up_c, top).Macro7 + (service, mu6).Macro5; |
|||
#Macro7 = (handoff_down, lambda1).Macro7 + (handoff_up, top).Macro7 + (handoff_in_up_c, top).Macro7 |
|||
+ (handoff_out_up_c, top).Macro7 + (service, mu7).Macro6; |
|||
|
|||
|
|||
#Micro0 = (in, lambda2).Micro1 + (handoff_out_c, top).Micro1 + (handoff_down, top).Micro1; |
|||
#Micro1 = (in, lambda2).Micro2 + (handoff_out_c, top).Micro2 + (handoff_in_up_c, alpha).Micro0 |
|||
+ (handoff_in_c, alpha).Micro0 + (service, mu).Micro0 + (handoff_down, top).Micro2; |
|||
#Micro2 = (in, lambda2).Micro3 + (handoff_out_c, top).Micro3 + (handoff_in_up_c, alpha2).Micro1 |
|||
+ (handoff_in_c, alpha2).Micro1 + (service, mu2).Micro1 + (handoff_down, top).Micro3; |
|||
#Micro3 = (in, lambda2).Micro4 + (handoff_out_c, top).Micro4 + (handoff_in_up_c, alpha3).Micro2 |
|||
+ (handoff_in_c, alpha3).Micro2 + (service, mu3).Micro2 + (handoff_down, top).Micro4; |
|||
#Micro4 = (in, lambda2).Micro5 + (handoff_out_c, top).Micro5 + (handoff_in_up_c, alpha4).Micro3 |
|||
+ (handoff_in_c, alpha4).Micro3 + (service, mu4).Micro3 + (handoff_down, top).Micro5; |
|||
#Micro5 = (in, lambda2).Micro6 + (handoff_out_c, top).Micro6 + (handoff_in_up_c, alpha5).Micro4 |
|||
+ (handoff_in_c, alpha5).Micro4 + (service, mu5).Micro4 + (handoff_down, top).Micro6; |
|||
#Micro6 = (in, lambda2).Micro7 + (handoff_out_c, top).Micro7 + (handoff_in_up_c, alpha6).Micro5 |
|||
+ (handoff_in_c, alpha6).Micro5 + (service, mu6).Micro5 + (handoff_down, top).Micro7; |
|||
#Micro7 = (handoff_up, lambda2).Micro7 + (handoff_out_up_c, top).Micro7 + (handoff_in_up_c, alpha7).Micro6 |
|||
+ (handoff_in_c, alpha7).Micro6 + (service, mu7).Micro6 + (handoff_down, top).Micro7; |
|||
|
|||
|
|||
#MicroC0 = (in, lambda3).MicroC1 + (handoff_in_c, top).MicroC1; |
|||
#MicroC1 = (in, lambda3).MicroC2 + (handoff_out_c, alpha).MicroC0 + (handoff_out_up_c, alpha).MicroC0 |
|||
+ (handoff_in_c, top).MicroC2 + (service, mu).MicroC0; |
|||
#MicroC2 = (in, lambda3).MicroC3 + (handoff_out_c, alpha2).MicroC1 + (handoff_out_up_c, alpha2).MicroC1 |
|||
+ (handoff_in_c, top).MicroC3 + (service, mu2).MicroC1; |
|||
#MicroC3 = (in, lambda3).MicroC4 + (handoff_out_c, alpha3).MicroC2 + (handoff_out_up_c, alpha3).MicroC2 |
|||
+ (handoff_in_c, top).MicroC4 + (service, mu3).MicroC2; |
|||
#MicroC4 = (in, lambda3).MicroC5 + (handoff_out_c, alpha4).MicroC3 + (handoff_out_up_c, alpha4).MicroC3 |
|||
+ (handoff_in_c, top).MicroC5 + (service, mu4).MicroC3; |
|||
#MicroC5 = (in, lambda3).MicroC6 + (handoff_out_c, alpha5).MicroC4 + (handoff_out_up_c, alpha5).MicroC4 |
|||
+ (handoff_in_c, top).MicroC6 + (service, mu5).MicroC4; |
|||
#MicroC6 = (in, lambda3).MicroC7 + (handoff_out_c, alpha6).MicroC5 + (handoff_out_up_c, alpha6).MicroC5 |
|||
+ (handoff_in_c, top).MicroC7 + (service, mu6).MicroC5; |
|||
#MicroC7 = (handoff_in_up_c, top).MicroC7 + (handoff_out_c, alpha7).MicroC6 + (service, mu7).MicroC6 |
|||
+ (handoff_up, lambda3).MicroC7 + (handoff_out_up_c, alpha7).MicroC6; |
|||
|
|||
|
|||
((Micro0<>Micro0<>Micro0<>Micro0) <handoff_in_c,handoff_out_c> MicroC0) <handoff_up,handoff_in_up_c,handoff_out_up_c> Macro0 |
|||
@ -1,237 +0,0 @@ |
|||
// Output from the PEPA-to-PRISM compiler |
|||
// Version 0.03.2 "Jean Armour Avenue" |
|||
// Released: 08-11-2002 |
|||
// |
|||
// Model file: TESTS/mobile |
|||
|
|||
// All PEPA models define CTMCs so mark this as a stochastic model |
|||
stochastic |
|||
|
|||
// The rates used in the model |
|||
rate lambda1 = 0.5; |
|||
rate lambda2 = 1.8; |
|||
rate lambda3 = 1.0; |
|||
rate mu = 0.008; |
|||
rate mu2 = 0.016; |
|||
rate mu3 = 0.024; |
|||
rate mu4 = 0.032; |
|||
rate mu5 = 0.040; |
|||
rate mu6 = 0.048; |
|||
rate mu7 = 0.054; |
|||
rate alpha = 0.018; |
|||
rate alpha2 = 0.036; |
|||
rate alpha3 = 0.054; |
|||
rate alpha4 = 0.072; |
|||
rate alpha5 = 0.090; |
|||
rate alpha6 = 0.108; |
|||
rate alpha7 = 0.126; |
|||
|
|||
|
|||
// Information about components inferred by the compiler |
|||
// during static analysis: |
|||
// |
|||
// interface Macro0 empty: only individual or passive activities |
|||
// interface MicroC0 |
|||
// activity handoff_out_c |
|||
// activity handoff_out_up_c |
|||
// activity handoff_up |
|||
// endinterface |
|||
|
|||
// interface Micro0 |
|||
// activity handoff_in_c |
|||
// activity handoff_in_up_c |
|||
// activity handoff_up |
|||
// endinterface |
|||
|
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const Micro0 = 0; |
|||
const Micro1 = 1; |
|||
const Micro2 = 2; |
|||
const Micro3 = 3; |
|||
const Micro4 = 4; |
|||
const Micro5 = 5; |
|||
const Micro6 = 6; |
|||
const Micro7 = 7; |
|||
module Micro0 |
|||
|
|||
Micro0_STATE : [0..7] init Micro0; |
|||
|
|||
[in] (Micro0_STATE=Micro0) -> lambda2 : (Micro0_STATE'=Micro1); |
|||
[handoff_out_c] (Micro0_STATE=Micro0) -> 1 : (Micro0_STATE'=Micro1); |
|||
[handoff_down] (Micro0_STATE=Micro0) -> 1 : (Micro0_STATE'=Micro1); |
|||
[in] (Micro0_STATE=Micro1) -> lambda2 : (Micro0_STATE'=Micro2); |
|||
[handoff_out_c] (Micro0_STATE=Micro1) -> 1 : (Micro0_STATE'=Micro2); |
|||
[handoff_in_up_c] (Micro0_STATE=Micro1) -> alpha : (Micro0_STATE'=Micro0); |
|||
[handoff_in_c] (Micro0_STATE=Micro1) -> alpha : (Micro0_STATE'=Micro0); |
|||
[service] (Micro0_STATE=Micro1) -> mu : (Micro0_STATE'=Micro0); |
|||
[handoff_down] (Micro0_STATE=Micro1) -> 1 : (Micro0_STATE'=Micro2); |
|||
[in] (Micro0_STATE=Micro2) -> lambda2 : (Micro0_STATE'=Micro3); |
|||
[handoff_out_c] (Micro0_STATE=Micro2) -> 1 : (Micro0_STATE'=Micro3); |
|||
[handoff_in_up_c] (Micro0_STATE=Micro2) -> alpha2 : (Micro0_STATE'=Micro1); |
|||
[handoff_in_c] (Micro0_STATE=Micro2) -> alpha2 : (Micro0_STATE'=Micro1); |
|||
[service] (Micro0_STATE=Micro2) -> mu2 : (Micro0_STATE'=Micro1); |
|||
[handoff_down] (Micro0_STATE=Micro2) -> 1 : (Micro0_STATE'=Micro3); |
|||
[in] (Micro0_STATE=Micro3) -> lambda2 : (Micro0_STATE'=Micro4); |
|||
[handoff_out_c] (Micro0_STATE=Micro3) -> 1 : (Micro0_STATE'=Micro4); |
|||
[handoff_in_up_c] (Micro0_STATE=Micro3) -> alpha3 : (Micro0_STATE'=Micro2); |
|||
[handoff_in_c] (Micro0_STATE=Micro3) -> alpha3 : (Micro0_STATE'=Micro2); |
|||
[service] (Micro0_STATE=Micro3) -> mu3 : (Micro0_STATE'=Micro2); |
|||
[handoff_down] (Micro0_STATE=Micro3) -> 1 : (Micro0_STATE'=Micro4); |
|||
[in] (Micro0_STATE=Micro4) -> lambda2 : (Micro0_STATE'=Micro5); |
|||
[handoff_out_c] (Micro0_STATE=Micro4) -> 1 : (Micro0_STATE'=Micro5); |
|||
[handoff_in_up_c] (Micro0_STATE=Micro4) -> alpha4 : (Micro0_STATE'=Micro3); |
|||
[handoff_in_c] (Micro0_STATE=Micro4) -> alpha4 : (Micro0_STATE'=Micro3); |
|||
[service] (Micro0_STATE=Micro4) -> mu4 : (Micro0_STATE'=Micro3); |
|||
[handoff_down] (Micro0_STATE=Micro4) -> 1 : (Micro0_STATE'=Micro5); |
|||
[in] (Micro0_STATE=Micro5) -> lambda2 : (Micro0_STATE'=Micro6); |
|||
[handoff_out_c] (Micro0_STATE=Micro5) -> 1 : (Micro0_STATE'=Micro6); |
|||
[handoff_in_up_c] (Micro0_STATE=Micro5) -> alpha5 : (Micro0_STATE'=Micro4); |
|||
[handoff_in_c] (Micro0_STATE=Micro5) -> alpha5 : (Micro0_STATE'=Micro4); |
|||
[service] (Micro0_STATE=Micro5) -> mu5 : (Micro0_STATE'=Micro4); |
|||
[handoff_down] (Micro0_STATE=Micro5) -> 1 : (Micro0_STATE'=Micro6); |
|||
[in] (Micro0_STATE=Micro6) -> lambda2 : (Micro0_STATE'=Micro7); |
|||
[handoff_out_c] (Micro0_STATE=Micro6) -> 1 : (Micro0_STATE'=Micro7); |
|||
[handoff_in_up_c] (Micro0_STATE=Micro6) -> alpha6 : (Micro0_STATE'=Micro5); |
|||
[handoff_in_c] (Micro0_STATE=Micro6) -> alpha6 : (Micro0_STATE'=Micro5); |
|||
[service] (Micro0_STATE=Micro6) -> mu6 : (Micro0_STATE'=Micro5); |
|||
[handoff_down] (Micro0_STATE=Micro6) -> 1 : (Micro0_STATE'=Micro7); |
|||
[handoff_up] (Micro0_STATE=Micro7) -> lambda2 : (Micro0_STATE'=Micro7); |
|||
[handoff_out_up_c] (Micro0_STATE=Micro7) -> 1 : (Micro0_STATE'=Micro7); |
|||
[handoff_in_up_c] (Micro0_STATE=Micro7) -> alpha7 : (Micro0_STATE'=Micro6); |
|||
[handoff_in_c] (Micro0_STATE=Micro7) -> alpha7 : (Micro0_STATE'=Micro6); |
|||
[service] (Micro0_STATE=Micro7) -> mu7 : (Micro0_STATE'=Micro6); |
|||
[handoff_down] (Micro0_STATE=Micro7) -> 1 : (Micro0_STATE'=Micro7); |
|||
|
|||
endmodule |
|||
|
|||
// We make another copy of module Micro0 |
|||
module Micro0_2 = Micro0[Micro0_STATE=Micro0_2_STATE] |
|||
endmodule |
|||
|
|||
// We make another copy of module Micro0 |
|||
module Micro0_3 = Micro0[Micro0_STATE=Micro0_3_STATE] |
|||
endmodule |
|||
|
|||
// We make another copy of module Micro0 |
|||
module Micro0_4 = Micro0[Micro0_STATE=Micro0_4_STATE] |
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const MicroC0 = 0; |
|||
const MicroC1 = 1; |
|||
const MicroC2 = 2; |
|||
const MicroC3 = 3; |
|||
const MicroC4 = 4; |
|||
const MicroC5 = 5; |
|||
const MicroC6 = 6; |
|||
const MicroC7 = 7; |
|||
module MicroC0 |
|||
|
|||
MicroC0_STATE : [0..7] init MicroC0; |
|||
|
|||
[in] (MicroC0_STATE=MicroC0) -> lambda3 : (MicroC0_STATE'=MicroC1); |
|||
[handoff_in_c] (MicroC0_STATE=MicroC0) -> 1 : (MicroC0_STATE'=MicroC1); |
|||
[in] (MicroC0_STATE=MicroC1) -> lambda3 : (MicroC0_STATE'=MicroC2); |
|||
[handoff_out_c] (MicroC0_STATE=MicroC1) -> alpha : (MicroC0_STATE'=MicroC0); |
|||
[handoff_out_up_c] (MicroC0_STATE=MicroC1) -> alpha : (MicroC0_STATE'=MicroC0); |
|||
[handoff_in_c] (MicroC0_STATE=MicroC1) -> 1 : (MicroC0_STATE'=MicroC2); |
|||
[service] (MicroC0_STATE=MicroC1) -> mu : (MicroC0_STATE'=MicroC0); |
|||
[in] (MicroC0_STATE=MicroC2) -> lambda3 : (MicroC0_STATE'=MicroC3); |
|||
[handoff_out_c] (MicroC0_STATE=MicroC2) -> alpha2 : (MicroC0_STATE'=MicroC1); |
|||
[handoff_out_up_c] (MicroC0_STATE=MicroC2) -> alpha2 : (MicroC0_STATE'=MicroC1); |
|||
[handoff_in_c] (MicroC0_STATE=MicroC2) -> 1 : (MicroC0_STATE'=MicroC3); |
|||
[service] (MicroC0_STATE=MicroC2) -> mu2 : (MicroC0_STATE'=MicroC1); |
|||
[in] (MicroC0_STATE=MicroC3) -> lambda3 : (MicroC0_STATE'=MicroC4); |
|||
[handoff_out_c] (MicroC0_STATE=MicroC3) -> alpha3 : (MicroC0_STATE'=MicroC2); |
|||
[handoff_out_up_c] (MicroC0_STATE=MicroC3) -> alpha3 : (MicroC0_STATE'=MicroC2); |
|||
[handoff_in_c] (MicroC0_STATE=MicroC3) -> 1 : (MicroC0_STATE'=MicroC4); |
|||
[service] (MicroC0_STATE=MicroC3) -> mu3 : (MicroC0_STATE'=MicroC2); |
|||
[in] (MicroC0_STATE=MicroC4) -> lambda3 : (MicroC0_STATE'=MicroC5); |
|||
[handoff_out_c] (MicroC0_STATE=MicroC4) -> alpha4 : (MicroC0_STATE'=MicroC3); |
|||
[handoff_out_up_c] (MicroC0_STATE=MicroC4) -> alpha4 : (MicroC0_STATE'=MicroC3); |
|||
[handoff_in_c] (MicroC0_STATE=MicroC4) -> 1 : (MicroC0_STATE'=MicroC5); |
|||
[service] (MicroC0_STATE=MicroC4) -> mu4 : (MicroC0_STATE'=MicroC3); |
|||
[in] (MicroC0_STATE=MicroC5) -> lambda3 : (MicroC0_STATE'=MicroC6); |
|||
[handoff_out_c] (MicroC0_STATE=MicroC5) -> alpha5 : (MicroC0_STATE'=MicroC4); |
|||
[handoff_out_up_c] (MicroC0_STATE=MicroC5) -> alpha5 : (MicroC0_STATE'=MicroC4); |
|||
[handoff_in_c] (MicroC0_STATE=MicroC5) -> 1 : (MicroC0_STATE'=MicroC6); |
|||
[service] (MicroC0_STATE=MicroC5) -> mu5 : (MicroC0_STATE'=MicroC4); |
|||
[in] (MicroC0_STATE=MicroC6) -> lambda3 : (MicroC0_STATE'=MicroC7); |
|||
[handoff_out_c] (MicroC0_STATE=MicroC6) -> alpha6 : (MicroC0_STATE'=MicroC5); |
|||
[handoff_out_up_c] (MicroC0_STATE=MicroC6) -> alpha6 : (MicroC0_STATE'=MicroC5); |
|||
[handoff_in_c] (MicroC0_STATE=MicroC6) -> 1 : (MicroC0_STATE'=MicroC7); |
|||
[service] (MicroC0_STATE=MicroC6) -> mu6 : (MicroC0_STATE'=MicroC5); |
|||
[handoff_in_up_c] (MicroC0_STATE=MicroC7) -> 1 : (MicroC0_STATE'=MicroC7); |
|||
[handoff_out_c] (MicroC0_STATE=MicroC7) -> alpha7 : (MicroC0_STATE'=MicroC6); |
|||
[service] (MicroC0_STATE=MicroC7) -> mu7 : (MicroC0_STATE'=MicroC6); |
|||
[handoff_up] (MicroC0_STATE=MicroC7) -> lambda3 : (MicroC0_STATE'=MicroC7); |
|||
[handoff_out_up_c] (MicroC0_STATE=MicroC7) -> alpha7 : (MicroC0_STATE'=MicroC6); |
|||
|
|||
endmodule |
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const Macro0 = 0; |
|||
const Macro1 = 1; |
|||
const Macro2 = 2; |
|||
const Macro3 = 3; |
|||
const Macro4 = 4; |
|||
const Macro5 = 5; |
|||
const Macro6 = 6; |
|||
const Macro7 = 7; |
|||
module Macro0 |
|||
|
|||
Macro0_STATE : [0..7] init Macro0; |
|||
|
|||
[in] (Macro0_STATE=Macro0) -> lambda1 : (Macro0_STATE'=Macro1); |
|||
[handoff_up] (Macro0_STATE=Macro0) -> 1 : (Macro0_STATE'=Macro1); |
|||
[handoff_in_up_c] (Macro0_STATE=Macro0) -> 1 : (Macro0_STATE'=Macro1); |
|||
[handoff_out_up_c] (Macro0_STATE=Macro0) -> 1 : (Macro0_STATE'=Macro1); |
|||
[in] (Macro0_STATE=Macro1) -> lambda1 : (Macro0_STATE'=Macro2); |
|||
[handoff_up] (Macro0_STATE=Macro1) -> 1 : (Macro0_STATE'=Macro2); |
|||
[handoff_in_up_c] (Macro0_STATE=Macro1) -> 1 : (Macro0_STATE'=Macro2); |
|||
[handoff_out_up_c] (Macro0_STATE=Macro1) -> 1 : (Macro0_STATE'=Macro2); |
|||
[service] (Macro0_STATE=Macro1) -> mu : (Macro0_STATE'=Macro0); |
|||
[in] (Macro0_STATE=Macro2) -> lambda1 : (Macro0_STATE'=Macro3); |
|||
[handoff_up] (Macro0_STATE=Macro2) -> 1 : (Macro0_STATE'=Macro3); |
|||
[handoff_in_up_c] (Macro0_STATE=Macro2) -> 1 : (Macro0_STATE'=Macro3); |
|||
[handoff_out_up_c] (Macro0_STATE=Macro2) -> 1 : (Macro0_STATE'=Macro3); |
|||
[service] (Macro0_STATE=Macro2) -> mu2 : (Macro0_STATE'=Macro1); |
|||
[in] (Macro0_STATE=Macro3) -> lambda1 : (Macro0_STATE'=Macro4); |
|||
[handoff_up] (Macro0_STATE=Macro3) -> 1 : (Macro0_STATE'=Macro4); |
|||
[handoff_in_up_c] (Macro0_STATE=Macro3) -> 1 : (Macro0_STATE'=Macro4); |
|||
[handoff_out_up_c] (Macro0_STATE=Macro3) -> 1 : (Macro0_STATE'=Macro4); |
|||
[service] (Macro0_STATE=Macro3) -> mu3 : (Macro0_STATE'=Macro2); |
|||
[in] (Macro0_STATE=Macro4) -> lambda1 : (Macro0_STATE'=Macro5); |
|||
[handoff_up] (Macro0_STATE=Macro4) -> 1 : (Macro0_STATE'=Macro5); |
|||
[handoff_in_up_c] (Macro0_STATE=Macro4) -> 1 : (Macro0_STATE'=Macro5); |
|||
[handoff_out_up_c] (Macro0_STATE=Macro4) -> 1 : (Macro0_STATE'=Macro5); |
|||
[service] (Macro0_STATE=Macro4) -> mu4 : (Macro0_STATE'=Macro3); |
|||
[in] (Macro0_STATE=Macro5) -> lambda1 : (Macro0_STATE'=Macro6); |
|||
[handoff_up] (Macro0_STATE=Macro5) -> 1 : (Macro0_STATE'=Macro6); |
|||
[handoff_in_up_c] (Macro0_STATE=Macro5) -> 1 : (Macro0_STATE'=Macro6); |
|||
[handoff_out_up_c] (Macro0_STATE=Macro5) -> 1 : (Macro0_STATE'=Macro6); |
|||
[service] (Macro0_STATE=Macro5) -> mu5 : (Macro0_STATE'=Macro4); |
|||
[in] (Macro0_STATE=Macro6) -> lambda1 : (Macro0_STATE'=Macro7); |
|||
[handoff_up] (Macro0_STATE=Macro6) -> 1 : (Macro0_STATE'=Macro7); |
|||
[handoff_in_up_c] (Macro0_STATE=Macro6) -> 1 : (Macro0_STATE'=Macro7); |
|||
[handoff_out_up_c] (Macro0_STATE=Macro6) -> 1 : (Macro0_STATE'=Macro7); |
|||
[service] (Macro0_STATE=Macro6) -> mu6 : (Macro0_STATE'=Macro5); |
|||
[handoff_down] (Macro0_STATE=Macro7) -> lambda1 : (Macro0_STATE'=Macro7); |
|||
[handoff_up] (Macro0_STATE=Macro7) -> 1 : (Macro0_STATE'=Macro7); |
|||
[handoff_in_up_c] (Macro0_STATE=Macro7) -> 1 : (Macro0_STATE'=Macro7); |
|||
[handoff_out_up_c] (Macro0_STATE=Macro7) -> 1 : (Macro0_STATE'=Macro7); |
|||
[service] (Macro0_STATE=Macro7) -> mu7 : (Macro0_STATE'=Macro6); |
|||
|
|||
endmodule |
|||
|
|||
|
|||
// The system equation |
|||
system |
|||
(((Micro0 ||| (Micro0_2 ||| (Micro0_3 ||| Micro0_4))) |[handoff_in_c, handoff_out_c]| MicroC0) |[handoff_up, handoff_in_up_c, handoff_out_up_c]| Macro0) |
|||
endsystem |
|||
|
|||
// End of output from the PEPA-to-PRISM compiler |
|||
@ -1,12 +0,0 @@ |
|||
r = 1.0; |
|||
t = 1.56; |
|||
|
|||
P = (a, r).P2; |
|||
P2 = (b, t).P; |
|||
|
|||
P <> P |
|||
|
|||
|
|||
|
|||
|
|||
|
|||
@ -1,45 +0,0 @@ |
|||
// Output from the PEPA-to-PRISM compiler |
|||
// Version 0.03.2 "Jean Armour Avenue" |
|||
// Released: 08-11-2002 |
|||
// |
|||
// Model file: TESTS/small |
|||
|
|||
// All PEPA models define CTMCs so mark this as a stochastic model |
|||
stochastic |
|||
|
|||
// The rates used in the model |
|||
rate r = 1.0; |
|||
rate t = 1.56; |
|||
|
|||
|
|||
// Information about components inferred by the compiler |
|||
// during static analysis: |
|||
// |
|||
|
|||
// interface P empty: only individual or passive activities |
|||
|
|||
|
|||
// Descriptive names for the local states of |
|||
// this module, taken from the PEPA input model |
|||
const P = 0; |
|||
const P2 = 1; |
|||
module P |
|||
|
|||
P_STATE : [0..1] init P; |
|||
|
|||
[a] (P_STATE=P) -> r : (P_STATE'=P2); |
|||
[b] (P_STATE=P2) -> t : (P_STATE'=P); |
|||
|
|||
endmodule |
|||
|
|||
// We make another copy of module P |
|||
module P_2 = P[P_STATE=P_2_STATE] |
|||
endmodule |
|||
|
|||
|
|||
// The system equation |
|||
system |
|||
(P ||| P_2) |
|||
endsystem |
|||
|
|||
// End of output from the PEPA-to-PRISM compiler |
|||
@ -1,8 +0,0 @@ |
|||
(* |
|||
File: pepa2prism.sml |
|||
|
|||
Used to compile the PEPA to PRISM Compiler with Moscow ML 2.00 (June 2000) |
|||
on Linux machines. |
|||
*) |
|||
|
|||
val _ = PEPA2PRISM.main (CommandLine.arguments ()); |
|||
@ -1,16 +0,0 @@ |
|||
|
|||
"# This is a script which compiles the PEPA to PRISM compiler." |
|||
|
|||
sourcepath /home/stg/pub/pwb/COMPILER/0.03.2 |
|||
|
|||
classpath /home/stg/java/java1.1.6/classes.zip |
|||
|
|||
classpath + /home/stg/pub/pwb/COMPILER/0.03.2/JAVA |
|||
|
|||
"echo Compiling the PEPA to PRISM compiler ... as pepa.zip " |
|||
|
|||
make pepa.T pepa |
|||
|
|||
"echo Compilation of the PEPA to PRISM compiler finished, exiting MLj. " |
|||
|
|||
quit |
|||
@ -1,43 +0,0 @@ |
|||
(* |
|||
File: pepa.sml |
|||
|
|||
This is the root file for the MLj compilation process and |
|||
refers the compiler to the PEPA2PRISM Standard ML structure. |
|||
|
|||
This version of the PEPA compiler compiles with MLj 0.1, |
|||
but not 0.2 |
|||
*) |
|||
|
|||
structure pepa = struct |
|||
|
|||
_public _classtype T |
|||
{ |
|||
|
|||
_public _static _final _method "compile" (fileName : Java.String option) : Java.String = |
|||
case fileName of |
|||
NONE => |
|||
Error.fatal_error "File name supplied for compilation was null" |
|||
| SOME fN => |
|||
Java.fromString (PEPA2PRISM.compile (Java.toString fN)) |
|||
|
|||
|
|||
_public _static _final _method "main" (env : Java.String option Java.array option) = |
|||
case env of |
|||
NONE => |
|||
PEPA2PRISM.main [] |
|||
| SOME env' => |
|||
let |
|||
val array = Java.toArray env' |
|||
in |
|||
if Array.length array = 0 |
|||
then PEPA2PRISM.main [] |
|||
else |
|||
case Array.sub(array, 0) of |
|||
NONE => PEPA2PRISM.main [] |
|||
| SOME jstr => |
|||
PEPA2PRISM.main [Java.toString jstr] |
|||
end |
|||
} |
|||
|
|||
|
|||
end; |
|||
@ -1,23 +0,0 @@ |
|||
Group is |
|||
Debugging.sig |
|||
Debugging.sml |
|||
Error.sig |
|||
Error.sml |
|||
Files.sig |
|||
Files.sml |
|||
Lexer.sig |
|||
Lexer.sml |
|||
Sort.sig |
|||
Sort.sml |
|||
Semantic.sig |
|||
Semantic.sml |
|||
Alphabets.sig |
|||
Alphabets.sml |
|||
PEPA2PRISM.sig |
|||
PEPA2PRISM.sml |
|||
Parser.sig |
|||
Parser.sml |
|||
Pepa.sig |
|||
Pepa.sml |
|||
Prettyprinter.sig |
|||
Prettyprinter.sml |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue