AORTA: Adding Organizational Reasoning to Agents
AORTA is an organizational reasoning component that can be integrated into the agent's reasoning mechanism, allowing it to reason about (and act upon) regulations specified by an organizational model using simple reasoning rules. Read more about AORTA here.
The project consists of the following:
- metamodel: The AORTA metamodel
- framework: The AORTA framework
- gui: GUI for the execution of AORTA agents
- jason: The integration with Jason
- jeditplugin: A plugin for JEdit for Jason
- apapl: Integration with 2APL
- Model checking
- ajpf2014: A modified version of AJPF to incorporate organizational properties as used in AORTA.
- aorta4ail: Implementation of AORTA operational semantics in AIL for optimized model checking.
- modelchecker: A model checker for AORTA using AJPF. Enables verification of AIL-systems integrated with AORTA (but without optimizations).
- examples: A collection of smaller example programs that can be run in AORTA+Jason or AORTA+2APL
- bw4t: An example usage of the jason-integration using Blocks World for Teams
- Organizational modeling
- opera: A translator from the OperA model to the AORTA metamodel
- moise: A translator from the Moise+ model to the AORTA metamodel
AORTA should be built using at least Java 7 (and exactly Java 7 to use the model checker).
Integration with Jason
The jeditplugin includes a build-configuration that creates a jar including AORTA and all dependencies. This jar (aorta-standalone.jar) furthermore comes with an installer, which installs AORTA into an existing Jason installation directory.
The installer is created using
ant make-installer in the jeditplugin folder and creates a new folder
installer containing the jar.
It can be run with the following command:
java -jar aorta-standalone.jar install <Jason-location>
The modelchecker works as a JPF plugin. It furthermore includes a build-configuration that creates a jar with all dependencies. This jar (in the folder
standalone) can be run as follows:
java -jar aorta-modelchecker.jar AIL-file [PSL-file] [p=Propertyname] [m=Modelfile] [-save]
If no PSL-file is provided, the system is executed normally. Otherwise, modelchecking using JPF is performed. The jar should be executed in the working directory of the system to be verified. To model check a specific property in the PSL-file, use
p=Propertyname. To generate a model of the entire system (use with precaution, can get quite large), use
p=Propertyname m=Modelfile -save (will be generated using the property specified by
Propertyname). To use the model file afterwards instead of running the system, use
Setup of the modelchecking system
The system relies on JPF and should therefore be setup as follows:
Download and unzip AORTA
Install JPF-Core (download and build from JPF repository)
Edit site.properties in ~/.jpf to include the following line:
mcapl = <Parent of AORTA project dir>/aorta/ajpf2014
Run the JAR file as specified above to verify the system in AIL-file using all the properties in PSL-file