Skip to content
Integration Property Language
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
.settings
gradle
org.xtext.example.ipl.ide
org.xtext.example.ipl.prism.lib
org.xtext.example.ipl.prism.plugin
org.xtext.example.ipl.target
org.xtext.example.ipl.tests
org.xtext.example.ipl.ui.tests
org.xtext.example.ipl.ui
org.xtext.example.ipl.viewgen
org.xtext.example.ipl.web
org.xtext.example.ipl.z3
org.xtext.example.ipl
.gitignore
.project
README.md
build.gradle
gradlew
gradlew.bat
pom.xml
settings.gradle

README.md

IPL: an Integration Property Language for Multiple Models

Development build setup

Prerequisites to have before installing IPL: Java 1.8.

Prerequisites to be installed below: Eclipse Oxygen 4.7.1a, EMF 2.13.0, Xtext SDK 2.12.0, OSATE 2.3.0.

  1. Download an appropriate Eclipse Installer for your system.

  2. Choose advanced setup and Eclipse Modeling Tools - Oxygen 1a (4.7.1a). It is likely that IPL would work with later releases of Oxygen too.

  3. On the Projects page, add the setup URL for OSATE 2.3.0 and click through the rest of the dialog. It will install Xtext, OSATE, and many relevant dependencies. You can also use the latest OSATE setup URL at your own risk.

Steps 1-3 are also described in more detail with minor deviations (a different install URL) on the OSATE2 setup page.

  1. Import this project into Eclipse: File → Import → Git → Projects from Git.

    • It along comes with its major dependencies: z3 SMT solver and Prism model checker.
    • z3 comes with a binary in org.xtext.example.ipl.z3, which is directly called by IPL. You can replace this binary with a different verion.
    • All the Prism model checker dependencies (including static and shared libraries) are provided in the ipl.prism.lib project. IPL is known to work with the version 4.4.beta of Prism. If you wish to adjust them, change variables LD_LIBRARY_PATH (should point to share library *.so files) and PRISM_LIB_PATH (should point to the HOA script and a jar of the Rabinizer tool).
  2. Build the IPL language infrastructure by running the GenerateIPL run configuration. Alternatively, you can directly run the org.xtext.example.ipl/src/org/xtext/example/ipl/GenerateIPL.mwe2 script (Right-Click on the file -> Run as -> MWE2 Workflow). Refresh and clean all the projects. It should build automatically.

  3. Use the provided launch file "IPL Eclipse Application" run configuration to start an Eclipse version with IPL support.

  4. Download IPL projects and import them in the launched verion of the Eclipse.

  5. To run IPL verification, you can click the IPL verification button while a .ipl file is open or selected. Alternatively, you can use the native Eclipse build. It is recommended that you turn off automatic building and target specific files since verification can take some time.

  6. If you want to generate AADL views or Prism models from json maps, run the main methods in org.xtext.example.ipl.viewgen/src/org/xtext/example/ipl/viewgen/map/MapTranslatorAadl.java and /org.xtext.example.ipl.viewgen/src/org/xtext/example/ipl/viewgen/map/MapTranslatorPrism.java, respectively.

    • Their launch files are also provided with in the repository.
    • You will need to adjust paths in the environment variables for these generators. MAP_DIR should point to the directory with input maps. PRISM_OUT_DIR and AADL_OUT_DIR should point to the directories where generated Prism and AADL models are put, respectively. None of these paths should end with a '/'.

User build setup

TBA.

Troubleshooting

Q: Which OSATE projects are necesary to run IPL?
A: All of the projects in the osate2-core working set and all in the osate-ge set except org.osate.ge.ba and org.osate.ge.errormodel. All the other working sets/repos from the Oomph setup are optional.

Q: I am getting bundle and compiler errors in OSATE2 code, including being unable to resolve eclipse.jdt.core.
A: Try switching the target platform in Preferences -> Plug-in Development -> Target Platform from "Modular Target" to "Running Platform." If this fixes the errors, you will want to make this change permanent by preventing Oomph from running the startup task that sets the target platform back to "Modular Target." Although that can be done in various ways, the easiest one is to delete two Eclipse plugins: Oomph Targlets and Oomph Setup Targlets.

Q: I am getting parameter value and artifact transfer errors related to Maven and/or Tycho.
A: Delete the failed artifacts and update IPL main project's Maven as described in this post.

Contacts

You can’t perform that action at this time.