The official site of P

The semantics of P

The P Tutorial

To use the parser you must run the maude/parser/p2maude.sh script. This script gets 4 parameters:

./p2maude.sh <module_name> <p_maude_semantic_file> <p_project_folder> <output_maude_file>

where

• <module_name> is the name that the Maude module will have.
• <p_maude_semantic_file> is the path to the Maude semantics of P (the p-0.5.maude file).
• <p_project_folder> is the url of the project in P that will be compiled and <output_maude_file> is the url of the Maude file that will be generated. An example of the execution would be something like:

  ./p2maude.sh CLIENT-SERVER ../../p-0.5.maude ../../Tutorial/1_ClientServer/ ../runs/ClientServer/client-server.maude
  

The script will take the files with .p extension in the PSrc, PSpec, and PTst folders of the P project folder and will generate the corresponding Maude module in the specified output file. This file will also include a module CLIENT-SERVER-RUN providing an operator init that initializes the system with all functions, tests and machines in the project.

To execute the semantics of P we just need to load the file generated by the parser

% maude client-server.maude 

Then, we just need to run the test case we are interested in using the execute operator on the initial init system:

Maude> frew [1000] execute(tcMultipleClients, init) .
frewrite [1000] in CLIENT-SERVER-RUN : execute(tcMultipleClients, init) .
rewrites: 1012 in 4ms cpu (4ms real) (237837 rewrites/second)
result SystemExecState: 
  ...

Alternatively, one can use a file loading the client-server.maude and then running the commands as in

% maude client-server-run.maude 

To execute the smc, we need the observation operations and the formula. The CLIENT-SERVER-PREDS module in the client-server-preds.maude file define several propositions. Specifically, it defines a proposition all clients at Y that becomes true if all client machines are in the Y state. Then, Quatex formulas must be defined. For example, the formula.quatex file contains the following definition

Steps() = if (s.rval("State |= all clients at NoMoneyToWithDraw"))
          then s.rval("steps")
          else # Steps() 
          fi;

eval E[Steps () ];

It calculates the number of steps taken until all clients in the are in the NoMoneyToWithdraw state. Given these files, we may use umaudemc o check the property on the tcSingleClients test case as follows.

% umaudemc scheck client-server-preds.maude 'execute(tcMultipleClients, init)' formula.quatex -a 0.999

Number of simulations = 30
  μ = 449.53333333333336        σ = 197.83373955356325        r = 0.0456607423753905

There are detailed instructions on how to run each of the examples in P's Tutorial at: ClientServer, EspressoMachine, TwoPhaseCommit,

There is a list of known issues.