README.txt 1.33 KB
Newer Older
1 2
Usage: ./ <FILENAME>.psl

Andrew's avatar
Andrew committed

Andrew's avatar
Andrew committed
5 6 7 8 9 10 11 12 13 14 15 16 17 18
./ <FILENAME>.sh

The difference is that the second command also automatically loads the 
generated Maude file into Maude-NPA, along with all the other files that
Maude-NPA needs to run properly, using the version of Maude included in the 
repository (maude27 as of May 14 2015). Note that if you invoke the shell
script, then Maude-NPA will be loaded whether or not the PSL script 
successfully executes. So invoking is recommended until the 
specification is well-formed.

The program will generate one files: 

19 20
contains the Maude-NPA modules that can be loaded into the Maude-NPA.

Andrew's avatar
Andrew committed
21 22
Note that although the translation program itself works with Maude 2.6, the 
Andrew's avatar
Andrew committed
24 25 26 27 28 29
that the generated modules are compatible with relies on a version of Maude 
that is
not-quite-ready for release. Therefore, in addition to the translation code, 
is an experimental version of Maude, the Maude prelude, and the Maude-NPA that 
these modules are compatible with. 
30 31 32

To load <FILENAME>.maude into the Maude-NPA, type:

Andrew's avatar
Andrew committed
./maude27 -no-prelude prelude.maude maude-npa.maude <FILENAME>.maude
34 35 36 37 38

For more details about PSL, see psl_description.pdf (a draft of Andrew Cholewa's
Spring 2015 Masters Thesis at University of Illinois at Urbana-Champaign), 
included with this repository.