[Mcapl-users] short guide to installing MCAPL

[Webster, M. <M.W...@li...>]

Hi all,

A few months ago I wrote a short guide to installing MCAPL. It's not comprehensive, but the method described worked for me. Let me know if you have any questions, comments, etc.!

Regards,
Matt

INSTALLING MCAPL - Nov 2010
Matt Webster - ma...@li...
======================================

Using:
# Fedora Linux 10.
# Fedora Eclipse 3.4.1 (build 20080911-1700).
# Subclipse for Eclipse.
# svn at the command line.
# Antlr parser generator.

======================================

# Checkout Java PathFinder revision 1000:
svn checkout https://javapathfinder.svn.sourceforge.net/svnroot/javapathfinder -r 1000

# Import an Existing Project into Workspace. Use the directory containing the javapathfinder trunk.

# Checkout the following Subversion Project using Subclipse:
  https://mcapl.svn.sourcefource.net/svnroot/mcapl
(I checked out revision 185.) Checkout the root of the repository into your Eclipse project.

# Add JPF to the Build Path and the Project References of the MCAPL project.

# Add antlrworks-1.4.jar (download from http://www.antlr.org/) as an External JAR.

# Add eis-0.2-lib.jar (in the MCAPL/lib directory) as an External JAR.

# Find the class MCAPLTestRig.java. Edit the line: 

  String jpfbasedir = "/Users/lad/Documents/workspace_helios/javapathfinder-trunk/";

so that it points to the directory containing the JPF trunk.

# Installation is complete.

TESTING
=======

# Run the file
  MCAPLProject/examples/gwendolen/auctions/basic/AuctionMAS.java
You should get output similar to this, showing that the MCAPL software is working:

--
Initialising 2 bidders
entered begin
Number: 1
Incoming: 0,1,
Old: ~B(ag3,win),~T R ~B(ag3,win),
Next: ~T R ~B(ag3,win),
 Property Accepting: true
 Empty Next: false

Number: 1
Incoming: 0,1,
Old: ~B(ag3,win),~T R ~B(ag3,win),
Next: ~T R ~B(ag3,win),
 Property Accepting: true
 Empty Next: false

Selecting state numbered 1 from 1
starting agentThread-2
starting agentThread-3
ag3
starting agentThread-4
ag3 done send(tell:bid(200.0,ag3), ag1)
ag2 done send(tell:bid(100.0,ag2), ag1)
bid(100.0,ag2)
ag1
ag1
bid(200.0,ag3)
ag1 done send(tell:win, ag3)
win
Always true from now on
ag1
--


# Now run the file 
  MCAPLProject/examples/gwendolen/auctions/basic/BasicAuctionTestRig.java
You should get output similar to this, showing that the MCAPL model checker is working.

...

2 BIDDERS

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       0:00:10
states:             new=36, visited=28, backtracked=63, end=0
search:             maxDepth=7, constraints=0
choice generators:  thread=37, data=0
heap:               gc=326, new=155771, free=146575
instructions:       14825274
max memory:         145MB
loaded code:        classes=260, methods=3786

====================================================== search finished: 11/14/10 3:46 PM

...