This file describes the instruction for installing ParTypes on a Windows VM on OSX.

OS: Windows

Prerequisites:

1. install VCC
   a. download VCC from http://vcc.codeplex.com/
   b. install Prerequisites according to instructions 
	  from http://vcc.codeplex.com/wikipage?title=Install&referringTitle=Home
	  IMPORTANT note: do NOT install VS 2015 or later, stick to VS 2010 or 2012
   c. install VCC by running the installation binary
   
2. java 1.8 (32-bit)
   IMPORTANT note: only works with 32-bit java
   install jdk 1.8 and configure environment variables 
   (JAVA_HOME, CLASSPATH, PATH, etc) appropriately
   
Install ParTypes:
(Reference: http://download.gloss.di.fc.ul.pt/ParTypes/ArtifactOverview.pdf)

1. download ParTypes artifact for OOPSLA 2015 from
   http://download.gloss.di.fc.ul.pt/ParTypes/ParTypes.zip
   
2. unzip the file to C:\;

3. append the text 
   ;c:\ParTypes\software\ParTypesVCC\bin;c:\ParTypes\software\z3-4.3.2-x86-win\bin 
   to environment variable "Path"
   
4. start Eclipse, from C:\ParTypes, use C:\ParTypes\workspace
   as the default workspace

5. in Eclipse, go to Run -> External Tools -> External Tools Configurations ...

6. in the configuration for "VCC Verification", make sure that "Location" is
   C:\ParTypes\software\ParTypesVCC\bin\mpiv.bat
   
7. the ParTypesVCC library from the artifact has a bug and you can use 
   ParTypesVCC-fix.zip to fix it:
   a. unzip ParTypesVCC-fix.zip
   b. modify mpiv.bat from C:\ParTypes\software\ParTypesVCC\bin\mpiv.bat
      by updating the path to the ParTypesVCC library

Test ParTypes:

1. in Eclipse, select the file pi.prot in Package Explorer view
   and press the Compiles the protocol to VCC format icon from the 
   tool bar (the blue "play" icon). 

2. select the pi-annotated.c file from the Package Explorer view 
   and press the Run VCC Verification icon.
   example output:
   
-- Executing: vcc /z3:/memory:4096 /time /f:main -p:"-Ic:\Users\zmanchun\Downloads\ParTypesVCC-fix\include" /p:-IC:\ParTypes\workspace\pi\src-gen C:\ParTypes\workspace\pi\src\pi-annotated.c
Verification of main succeeded. [3.36]
                         Total 11.405
                  FELT Visitor 1.436
                  Total Plugin 4.773
                       Prelude 0.281
                        Boogie 0.833
                    Boogie AST 0.000
                     Boogie AI 0.152
                Boogie Resolve 0.007
              Boogie Typecheck 0.123
                  VC Optimizer 0.000
           Boogie Verify Impl. 2.175
               Boogie Save BPL 0.000
                       Pruning 0.000
              AST transformers 0.725
-- Execution time: 17.20 seconds



   
