Project developed for Languages and Computational Models course (2011-2012), by Daniele Bellavista. Metamaude is a tool, written in maude, for Continuous-Time Markov Chain simulation and verification.

Manual, relation and code comment are in Italian. If someone is interested in english translation, contact me.

The project documentation is splitted in Relation and Documentation.

The project relation includes theory concepts about maude meta-level and PCTL/APMC, the description of CTMC and PCTL project and the comparison with PRISM.

meta-maude.relazione/Bellavista-MetaMaude_Relazione.pdf

Project manual contains the tool how-to

meta-maude.relazione/Bellavista-MetaMaude_Manuale.pdf

Maude code is contained into maude directory and it's organized as follow:

• CTMC.maude: CTMC syntax e simulation.
• PCTL.maude: PCTL formulae syntax e verification.
• CTMC-READERS_WRITERS.maude: READERS_WRITERS model.
• CTMC-BSF.maude: Bromosulftaleine model test.
• CTMC-MMCK.maude: code M/M/C/K system model.

The directory prism contains the PRISM code.

Simulation of the readers and writers model with 30 initial token, 1000 simulation steps, getting an overview every 100 step and using as random seed 213.

 start maude
 Maude> load CTMC.maude
 Maude> load PCTL.maude
 Maude> load CTMC-READERS_WRITERS.maude
 Maude> set print attribute on .
 Maude> red in CTMC-RW_SIMULATOR : simulate ( 30, 1000, 100, 213 ) .

Verification of the readers and writers model with 30 initial token that within 0.1 seconds, a write will be executed with a probability of 80% with 0.1 approximation, confidence 0.01, maximum depth 1000 and random seed 2353.

 start maude
 Maude> load CTMC.maude
 Maude> load PCTL.maude
 Maude> load CTMC-READERS_WRITERS.maude
 Maude> set print attribute on .
 Maude> red in CTMC-RW_VERIFIER : verify ( 30, P[0.8]( (TRUE)U[0.1](upTerm(< v( "write" , 1) >))), 0.1, 0.01, 1000, 2353) .