Skip to content

Integration with PMaude specification

Andrea Vandin edited this page Dec 14, 2021 · 6 revisions

How to integrate MultiVeStA with your PMaude specifications

  1. Please download

  2. Decompress the zip archive and replace multivesta.jar with the downloaded one.

  3. Look at what is contained in the archive

    • a readme file with all necessary information (README.txt)
    • a model of a dice in PMaude (dice.maude)
    • two multiquatex queries to study the probability of extracting
      • the face 1 (multiquatex/probExtract1.multiquatex), and
      • each face (multiquatex/probExtractEachFace.multiquatex)
    • example commands to perform different analysis using
      • Mac (runMultivestaMAC.sh)
      • linux 64 bits (runMultivestaLinux64.sh)
    • troubleshooting guides to solve problems that might arise on
      • Mac (troubleShootingMac.txt)
      • linux (troubleShootingLinux.txt)
  4. Open a command line/terminal from inside the PMaude folder, choose one of the commands from the sh files, and run it. You should get the expected results.

  5. Please run some of the experiments, and come back to us if you have any questions or comments.