Using BEG
There are two problems the tools addresses:
1. Generation of the missing environment: given a unit (and no environment), the tool generates the environment for it. There are two types of the environments the tool can generate:
- The most general drivers and stubs
- According to a provided specification
- LTL or Regular expression for drivers
- Java like language for stubs (descriptions of side-effects in the stubs)
2. Generation of the compact representation of the given envirnoment: given a unit and the implementation of the environment, the tool performs a static analysis of the environment and generates a safe compact representation for the environment classes according to the static analysis information.
Where to find it
I've installed
- a version of the tool in ~santos/EnvGen (I'll try to update it)
- script "envgen" in ~santos/bin
How to run it
- As long as ~santos/bin is in your path, you can just type envgen, it brings out the options menu (as well as envgen -help )
- To run the tool type "envgen [-options] <unit Java classes>"
- There are two basic modes the tool has:
- -s : generation of stubs
- by deafult the most general stubs are generated
- -se : performs side-effects analysis of the environment methods and generates stubs for top level environment methods.
- -k <int> : set the limit in k-limiting, default is 2
- -d :generation of drivers (default option)
- Universal (default option)
- -n <int>: specifes the number of threads created for the Universal driver. By default the tool constructs two threads.
- Synthesized (from LTL or RE)
- There are two differrent specification notations that can be used for description of drivers behavior
- general options:
- There are two different contexts for code generation
- -b : Bandera
- -j : JPF (default option)
- There are two ways to input the specification
- -sf <specfilename> : from a file
- -cl : from a command line
- Visibility of environment actions
- -a : generation of atomic blocks in the environment. This is helpful when one wants to conceal the actions of the environment from the model checker.
- Output directory
- -o <dirname> :puts all of the generated classes into a separate directory .This is useful for dumping java.swing or java.awt libraries into a separate directory.
- Debugging messages
- -debug : prints out exra messages