From 4401630dcf1b1cf19b7928eb680222f8633d68d4 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 1 Nov 2007 16:13:14 +0000 Subject: [PATCH] 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-cb519fbb1720 --- prism/src/pepa/src/Alphabets.sig | 13 - prism/src/pepa/src/Alphabets.sml | 54 -- prism/src/pepa/src/COPYING | 341 -------- prism/src/pepa/src/CommandLine.sig | 10 - prism/src/pepa/src/CommandLine.sml | 15 - prism/src/pepa/src/Debugging.sig | 18 - prism/src/pepa/src/Debugging.sml | 39 - prism/src/pepa/src/Derivatives.sig | 12 - prism/src/pepa/src/Derivatives.sml | 47 -- prism/src/pepa/src/Error.sig | 22 - prism/src/pepa/src/Error.sml | 54 -- prism/src/pepa/src/Extractor.sig | 11 - prism/src/pepa/src/Extractor.sml | 35 - prism/src/pepa/src/Files.sig | 17 - prism/src/pepa/src/Files.sml | 41 - prism/src/pepa/src/JAVA/Makefile | 5 - .../src/JAVA/pepa/compiler/InternalError.java | 10 - .../src/pepa/src/JAVA/pepa/compiler/Main.java | 60 -- prism/src/pepa/src/Lexer.sig | 18 - prism/src/pepa/src/Lexer.sml | 46 -- prism/src/pepa/src/Lists.sig | 14 - prism/src/pepa/src/Lists.sml | 28 - prism/src/pepa/src/Makefile | 13 - prism/src/pepa/src/Makefile.mosml | 71 -- prism/src/pepa/src/PEPA2PRISM.sig | 15 - prism/src/pepa/src/PEPA2PRISM.sml | 771 ------------------ prism/src/pepa/src/Parser.sig | 10 - prism/src/pepa/src/Parser.sml | 183 ----- prism/src/pepa/src/Pepa.sig | 33 - prism/src/pepa/src/Pepa.sml | 54 -- prism/src/pepa/src/Prettyprinter.sig | 12 - prism/src/pepa/src/Prettyprinter.sml | 88 -- prism/src/pepa/src/README | 59 -- prism/src/pepa/src/README.TOO | 22 - prism/src/pepa/src/Semantic.sig | 12 - prism/src/pepa/src/Semantic.sml | 154 ---- prism/src/pepa/src/Sort.sig | 11 - prism/src/pepa/src/Sort.sml | 24 - prism/src/pepa/src/TESTS/ERRORS/README | 8 - .../pepa/src/TESTS/ERRORS/activeactive.pepa | 7 - .../pepa/src/TESTS/ERRORS/ratemissing.pepa | 4 - prism/src/pepa/src/TESTS/README | 7 - prism/src/pepa/src/TESTS/auction.pepa | 110 --- prism/src/pepa/src/TESTS/auction_pepa.sm | 288 ------- prism/src/pepa/src/TESTS/badge.1.4.pepa | 22 - prism/src/pepa/src/TESTS/badge.1.4_pepa.sm | 121 --- prism/src/pepa/src/TESTS/hiding.pepa | 6 - prism/src/pepa/src/TESTS/hiding_pepa.sm | 44 - prism/src/pepa/src/TESTS/mobile.pepa | 78 -- prism/src/pepa/src/TESTS/mobile_pepa.sm | 237 ------ prism/src/pepa/src/TESTS/small.pepa | 12 - prism/src/pepa/src/TESTS/small_pepa.sm | 45 - prism/src/pepa/src/compiler.sml | 8 - prism/src/pepa/src/pepa.mlj | 16 - prism/src/pepa/src/pepa.renamed.sml | 43 - prism/src/pepa/src/sources.cm | 23 - 56 files changed, 3521 deletions(-) delete mode 100644 prism/src/pepa/src/Alphabets.sig delete mode 100644 prism/src/pepa/src/Alphabets.sml delete mode 100644 prism/src/pepa/src/COPYING delete mode 100644 prism/src/pepa/src/CommandLine.sig delete mode 100644 prism/src/pepa/src/CommandLine.sml delete mode 100644 prism/src/pepa/src/Debugging.sig delete mode 100644 prism/src/pepa/src/Debugging.sml delete mode 100644 prism/src/pepa/src/Derivatives.sig delete mode 100644 prism/src/pepa/src/Derivatives.sml delete mode 100644 prism/src/pepa/src/Error.sig delete mode 100644 prism/src/pepa/src/Error.sml delete mode 100644 prism/src/pepa/src/Extractor.sig delete mode 100644 prism/src/pepa/src/Extractor.sml delete mode 100644 prism/src/pepa/src/Files.sig delete mode 100644 prism/src/pepa/src/Files.sml delete mode 100644 prism/src/pepa/src/JAVA/Makefile delete mode 100644 prism/src/pepa/src/JAVA/pepa/compiler/InternalError.java delete mode 100644 prism/src/pepa/src/JAVA/pepa/compiler/Main.java delete mode 100644 prism/src/pepa/src/Lexer.sig delete mode 100644 prism/src/pepa/src/Lexer.sml delete mode 100644 prism/src/pepa/src/Lists.sig delete mode 100644 prism/src/pepa/src/Lists.sml delete mode 100644 prism/src/pepa/src/Makefile delete mode 100644 prism/src/pepa/src/Makefile.mosml delete mode 100644 prism/src/pepa/src/PEPA2PRISM.sig delete mode 100644 prism/src/pepa/src/PEPA2PRISM.sml delete mode 100644 prism/src/pepa/src/Parser.sig delete mode 100644 prism/src/pepa/src/Parser.sml delete mode 100644 prism/src/pepa/src/Pepa.sig delete mode 100644 prism/src/pepa/src/Pepa.sml delete mode 100644 prism/src/pepa/src/Prettyprinter.sig delete mode 100644 prism/src/pepa/src/Prettyprinter.sml delete mode 100644 prism/src/pepa/src/README delete mode 100644 prism/src/pepa/src/README.TOO delete mode 100644 prism/src/pepa/src/Semantic.sig delete mode 100644 prism/src/pepa/src/Semantic.sml delete mode 100644 prism/src/pepa/src/Sort.sig delete mode 100644 prism/src/pepa/src/Sort.sml delete mode 100644 prism/src/pepa/src/TESTS/ERRORS/README delete mode 100644 prism/src/pepa/src/TESTS/ERRORS/activeactive.pepa delete mode 100644 prism/src/pepa/src/TESTS/ERRORS/ratemissing.pepa delete mode 100644 prism/src/pepa/src/TESTS/README delete mode 100644 prism/src/pepa/src/TESTS/auction.pepa delete mode 100644 prism/src/pepa/src/TESTS/auction_pepa.sm delete mode 100644 prism/src/pepa/src/TESTS/badge.1.4.pepa delete mode 100644 prism/src/pepa/src/TESTS/badge.1.4_pepa.sm delete mode 100644 prism/src/pepa/src/TESTS/hiding.pepa delete mode 100644 prism/src/pepa/src/TESTS/hiding_pepa.sm delete mode 100644 prism/src/pepa/src/TESTS/mobile.pepa delete mode 100644 prism/src/pepa/src/TESTS/mobile_pepa.sm delete mode 100644 prism/src/pepa/src/TESTS/small.pepa delete mode 100644 prism/src/pepa/src/TESTS/small_pepa.sm delete mode 100644 prism/src/pepa/src/compiler.sml delete mode 100644 prism/src/pepa/src/pepa.mlj delete mode 100644 prism/src/pepa/src/pepa.renamed.sml delete mode 100644 prism/src/pepa/src/sources.cm diff --git a/prism/src/pepa/src/Alphabets.sig b/prism/src/pepa/src/Alphabets.sig deleted file mode 100644 index 7056ad0a..00000000 --- a/prism/src/pepa/src/Alphabets.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Alphabets.sml b/prism/src/pepa/src/Alphabets.sml deleted file mode 100644 index a962ea49..00000000 --- a/prism/src/pepa/src/Alphabets.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/COPYING b/prism/src/pepa/src/COPYING deleted file mode 100644 index 1942c433..00000000 --- a/prism/src/pepa/src/COPYING +++ /dev/null @@ -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. - - - Copyright (C) 19yy - - 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. - - , 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. diff --git a/prism/src/pepa/src/CommandLine.sig b/prism/src/pepa/src/CommandLine.sig deleted file mode 100644 index 8dc53e90..00000000 --- a/prism/src/pepa/src/CommandLine.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/CommandLine.sml b/prism/src/pepa/src/CommandLine.sml deleted file mode 100644 index 92a5ca88..00000000 --- a/prism/src/pepa/src/CommandLine.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Debugging.sig b/prism/src/pepa/src/Debugging.sig deleted file mode 100644 index 67ef47a3..00000000 --- a/prism/src/pepa/src/Debugging.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Debugging.sml b/prism/src/pepa/src/Debugging.sml deleted file mode 100644 index c8a584f6..00000000 --- a/prism/src/pepa/src/Debugging.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Derivatives.sig b/prism/src/pepa/src/Derivatives.sig deleted file mode 100644 index 4be69eac..00000000 --- a/prism/src/pepa/src/Derivatives.sig +++ /dev/null @@ -1,12 +0,0 @@ -(* - File: Derivatives.sig - -*) -signature Derivatives = -sig - - val lookup : string -> string list option - - val recordDerivatives : string * string list -> unit - -end; diff --git a/prism/src/pepa/src/Derivatives.sml b/prism/src/pepa/src/Derivatives.sml deleted file mode 100644 index 783529d4..00000000 --- a/prism/src/pepa/src/Derivatives.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Error.sig b/prism/src/pepa/src/Error.sig deleted file mode 100644 index c9fa4634..00000000 --- a/prism/src/pepa/src/Error.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Error.sml b/prism/src/pepa/src/Error.sml deleted file mode 100644 index 09d9f661..00000000 --- a/prism/src/pepa/src/Error.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Extractor.sig b/prism/src/pepa/src/Extractor.sig deleted file mode 100644 index 1aeacd06..00000000 --- a/prism/src/pepa/src/Extractor.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Extractor.sml b/prism/src/pepa/src/Extractor.sml deleted file mode 100644 index 26e303a3..00000000 --- a/prism/src/pepa/src/Extractor.sml +++ /dev/null @@ -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; - diff --git a/prism/src/pepa/src/Files.sig b/prism/src/pepa/src/Files.sig deleted file mode 100644 index c9aca996..00000000 --- a/prism/src/pepa/src/Files.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Files.sml b/prism/src/pepa/src/Files.sml deleted file mode 100644 index 31b18775..00000000 --- a/prism/src/pepa/src/Files.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/JAVA/Makefile b/prism/src/pepa/src/JAVA/Makefile deleted file mode 100644 index 2012c407..00000000 --- a/prism/src/pepa/src/JAVA/Makefile +++ /dev/null @@ -1,5 +0,0 @@ -all: - javac pepa/compiler/*.java - -run: - java -classpath .:../pepa.zip pepa.compiler.Main ../TESTS/auction.pepa diff --git a/prism/src/pepa/src/JAVA/pepa/compiler/InternalError.java b/prism/src/pepa/src/JAVA/pepa/compiler/InternalError.java deleted file mode 100644 index 3842edb9..00000000 --- a/prism/src/pepa/src/JAVA/pepa/compiler/InternalError.java +++ /dev/null @@ -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); - } - -} diff --git a/prism/src/pepa/src/JAVA/pepa/compiler/Main.java b/prism/src/pepa/src/JAVA/pepa/compiler/Main.java deleted file mode 100644 index b1e1adc1..00000000 --- a/prism/src/pepa/src/JAVA/pepa/compiler/Main.java +++ /dev/null @@ -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])); - } -} diff --git a/prism/src/pepa/src/Lexer.sig b/prism/src/pepa/src/Lexer.sig deleted file mode 100644 index 92f38972..00000000 --- a/prism/src/pepa/src/Lexer.sig +++ /dev/null @@ -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; - diff --git a/prism/src/pepa/src/Lexer.sml b/prism/src/pepa/src/Lexer.sml deleted file mode 100644 index faae35a2..00000000 --- a/prism/src/pepa/src/Lexer.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Lists.sig b/prism/src/pepa/src/Lists.sig deleted file mode 100644 index 1cca3a8a..00000000 --- a/prism/src/pepa/src/Lists.sig +++ /dev/null @@ -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; - diff --git a/prism/src/pepa/src/Lists.sml b/prism/src/pepa/src/Lists.sml deleted file mode 100644 index 63680214..00000000 --- a/prism/src/pepa/src/Lists.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Makefile b/prism/src/pepa/src/Makefile deleted file mode 100644 index cea18a84..00000000 --- a/prism/src/pepa/src/Makefile +++ /dev/null @@ -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 diff --git a/prism/src/pepa/src/Makefile.mosml b/prism/src/pepa/src/Makefile.mosml deleted file mode 100644 index 221dd910..00000000 --- a/prism/src/pepa/src/Makefile.mosml +++ /dev/null @@ -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 - diff --git a/prism/src/pepa/src/PEPA2PRISM.sig b/prism/src/pepa/src/PEPA2PRISM.sig deleted file mode 100644 index 4d9fd434..00000000 --- a/prism/src/pepa/src/PEPA2PRISM.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/PEPA2PRISM.sml b/prism/src/pepa/src/PEPA2PRISM.sml deleted file mode 100644 index 1ed8cb3d..00000000 --- a/prism/src/pepa/src/PEPA2PRISM.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Parser.sig b/prism/src/pepa/src/Parser.sig deleted file mode 100644 index db6b5ecf..00000000 --- a/prism/src/pepa/src/Parser.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Parser.sml b/prism/src/pepa/src/Parser.sml deleted file mode 100644 index baf977b3..00000000 --- a/prism/src/pepa/src/Parser.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Pepa.sig b/prism/src/pepa/src/Pepa.sig deleted file mode 100644 index b22031b6..00000000 --- a/prism/src/pepa/src/Pepa.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Pepa.sml b/prism/src/pepa/src/Pepa.sml deleted file mode 100644 index 7b5bb246..00000000 --- a/prism/src/pepa/src/Pepa.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Prettyprinter.sig b/prism/src/pepa/src/Prettyprinter.sig deleted file mode 100644 index 315ee354..00000000 --- a/prism/src/pepa/src/Prettyprinter.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Prettyprinter.sml b/prism/src/pepa/src/Prettyprinter.sml deleted file mode 100644 index cc1d2591..00000000 --- a/prism/src/pepa/src/Prettyprinter.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/README b/prism/src/pepa/src/README deleted file mode 100644 index 61f5a902..00000000 --- a/prism/src/pepa/src/README +++ /dev/null @@ -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. - diff --git a/prism/src/pepa/src/README.TOO b/prism/src/pepa/src/README.TOO deleted file mode 100644 index d0681cf6..00000000 --- a/prism/src/pepa/src/README.TOO +++ /dev/null @@ -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 diff --git a/prism/src/pepa/src/Semantic.sig b/prism/src/pepa/src/Semantic.sig deleted file mode 100644 index 98b3c300..00000000 --- a/prism/src/pepa/src/Semantic.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Semantic.sml b/prism/src/pepa/src/Semantic.sml deleted file mode 100644 index 7e11dcac..00000000 --- a/prism/src/pepa/src/Semantic.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Sort.sig b/prism/src/pepa/src/Sort.sig deleted file mode 100644 index 763cecbf..00000000 --- a/prism/src/pepa/src/Sort.sig +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/Sort.sml b/prism/src/pepa/src/Sort.sml deleted file mode 100644 index fb8c549f..00000000 --- a/prism/src/pepa/src/Sort.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/TESTS/ERRORS/README b/prism/src/pepa/src/TESTS/ERRORS/README deleted file mode 100644 index 44310cae..00000000 --- a/prism/src/pepa/src/TESTS/ERRORS/README +++ /dev/null @@ -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 -2-12-2002 - diff --git a/prism/src/pepa/src/TESTS/ERRORS/activeactive.pepa b/prism/src/pepa/src/TESTS/ERRORS/activeactive.pepa deleted file mode 100644 index 87a7eef6..00000000 --- a/prism/src/pepa/src/TESTS/ERRORS/activeactive.pepa +++ /dev/null @@ -1,7 +0,0 @@ -r = 1.0; -s = 2.0; - -P = (a,r).P; -Q = (a,s).Q; - -P Q diff --git a/prism/src/pepa/src/TESTS/ERRORS/ratemissing.pepa b/prism/src/pepa/src/TESTS/ERRORS/ratemissing.pepa deleted file mode 100644 index 0a022b44..00000000 --- a/prism/src/pepa/src/TESTS/ERRORS/ratemissing.pepa +++ /dev/null @@ -1,4 +0,0 @@ - -P = (a,r).P; - -P <> P diff --git a/prism/src/pepa/src/TESTS/README b/prism/src/pepa/src/TESTS/README deleted file mode 100644 index 0c94e277..00000000 --- a/prism/src/pepa/src/TESTS/README +++ /dev/null @@ -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 -2-12-2002 - diff --git a/prism/src/pepa/src/TESTS/auction.pepa b/prism/src/pepa/src/TESTS/auction.pepa deleted file mode 100644 index a1890375..00000000 --- a/prism/src/pepa/src/TESTS/auction.pepa +++ /dev/null @@ -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 -((Bidder <> Bidder) - TNode)) - (CNode (Bidder_CN <> Bidder_CN))) - Node -(Bidder <> Bidder) diff --git a/prism/src/pepa/src/TESTS/auction_pepa.sm b/prism/src/pepa/src/TESTS/auction_pepa.sm deleted file mode 100644 index 2f4b3816..00000000 --- a/prism/src/pepa/src/TESTS/auction_pepa.sm +++ /dev/null @@ -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 diff --git a/prism/src/pepa/src/TESTS/badge.1.4.pepa b/prism/src/pepa/src/TESTS/badge.1.4.pepa deleted file mode 100644 index 55b4ed3b..00000000 --- a/prism/src/pepa/src/TESTS/badge.1.4.pepa +++ /dev/null @@ -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 (S16 ((S14 DB14) P14)) diff --git a/prism/src/pepa/src/TESTS/badge.1.4_pepa.sm b/prism/src/pepa/src/TESTS/badge.1.4_pepa.sm deleted file mode 100644 index 89437be1..00000000 --- a/prism/src/pepa/src/TESTS/badge.1.4_pepa.sm +++ /dev/null @@ -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 diff --git a/prism/src/pepa/src/TESTS/hiding.pepa b/prism/src/pepa/src/TESTS/hiding.pepa deleted file mode 100644 index 544e99d5..00000000 --- a/prism/src/pepa/src/TESTS/hiding.pepa +++ /dev/null @@ -1,6 +0,0 @@ -r = 1.0; - -P = (a,r).P'; -P' = (a,r).P; - -(P / {a}) <> P diff --git a/prism/src/pepa/src/TESTS/hiding_pepa.sm b/prism/src/pepa/src/TESTS/hiding_pepa.sm deleted file mode 100644 index f917daf0..00000000 --- a/prism/src/pepa/src/TESTS/hiding_pepa.sm +++ /dev/null @@ -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 diff --git a/prism/src/pepa/src/TESTS/mobile.pepa b/prism/src/pepa/src/TESTS/mobile.pepa deleted file mode 100644 index 882e0269..00000000 --- a/prism/src/pepa/src/TESTS/mobile.pepa +++ /dev/null @@ -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) MicroC0) Macro0 diff --git a/prism/src/pepa/src/TESTS/mobile_pepa.sm b/prism/src/pepa/src/TESTS/mobile_pepa.sm deleted file mode 100644 index 4f382755..00000000 --- a/prism/src/pepa/src/TESTS/mobile_pepa.sm +++ /dev/null @@ -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 diff --git a/prism/src/pepa/src/TESTS/small.pepa b/prism/src/pepa/src/TESTS/small.pepa deleted file mode 100644 index f6195556..00000000 --- a/prism/src/pepa/src/TESTS/small.pepa +++ /dev/null @@ -1,12 +0,0 @@ -r = 1.0; -t = 1.56; - -P = (a, r).P2; -P2 = (b, t).P; - -P <> P - - - - - diff --git a/prism/src/pepa/src/TESTS/small_pepa.sm b/prism/src/pepa/src/TESTS/small_pepa.sm deleted file mode 100644 index fc8777dd..00000000 --- a/prism/src/pepa/src/TESTS/small_pepa.sm +++ /dev/null @@ -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 diff --git a/prism/src/pepa/src/compiler.sml b/prism/src/pepa/src/compiler.sml deleted file mode 100644 index ed17ef5c..00000000 --- a/prism/src/pepa/src/compiler.sml +++ /dev/null @@ -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 ()); diff --git a/prism/src/pepa/src/pepa.mlj b/prism/src/pepa/src/pepa.mlj deleted file mode 100644 index 2b266a40..00000000 --- a/prism/src/pepa/src/pepa.mlj +++ /dev/null @@ -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 diff --git a/prism/src/pepa/src/pepa.renamed.sml b/prism/src/pepa/src/pepa.renamed.sml deleted file mode 100644 index 1752b0f7..00000000 --- a/prism/src/pepa/src/pepa.renamed.sml +++ /dev/null @@ -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; diff --git a/prism/src/pepa/src/sources.cm b/prism/src/pepa/src/sources.cm deleted file mode 100644 index 0c7866f5..00000000 --- a/prism/src/pepa/src/sources.cm +++ /dev/null @@ -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