Project

General

Profile

Developer Installation

1. Java Compiler Version 8
2. Eclipse Base Installation
3. Initial workspace content check-out
4. Materializing the target platform and plugin sources
5. Starting AF3
6. FAQs

This Tutorial explains how to obtain the current development version of AutoFOCUS 3. We setup an Eclipse development environment and download the current development sources from the repository. Most of the work will be performed by buckminster, which is an Eclipse extension supporting workspace materialization. Note that the overall time of the setup highly depends on your internet connection, since most of the resolution and materialization process accesses remote repositories and update sites.

We will use two instances of Eclipse: one for compiling the sources and the other one for running AF3. We will start the second instance from within the first one. Therefore, we also need two Eclipse workspaces. In the scope of this tutorial we will call the first one build workspace and the second one runtime workspace.

It is important that you do this setup with a clean Eclipse installation and a clean build workspace. Reusing previous installations or workspaces has shown to be error-prone if buckminster is used.

Given you have no developer account with our repository, use the following authentication information when asked:

user proxy_svn, password dW09WmzRcCUF

Java Compiler Version 8

The AF3 source must be compiled using a Java compiler supporting Java Version 8. Make sure you have an appropriate compiler version.

Notes
  • You can use a 32 or 64-bit version of Java/Eclipse, but pay attention that running Eclipse in 32-bit mode requires a 32-bit Java and 64-bit Eclipse requires 64-bit Java.
  • On Windows 8.1 (x64), currently only Eclipse (x64) / JDK (x64) are supported. Otherwise, launching AF3 will result in an error that lwjgl.dll cannot be resolved.

Use the following link to get JDK8 without registration.
http://www.oracle.com/technetwork/java/javase/downloads/jdk8-downloads-2133151.html

Installation

Important: Do not install Eclipse nor its workspace in a path containing spaces, do not put spaces in the name of your Eclipse directory (e.g., "eclipse4" is ok, but not "eclipse 4").

Eclipse Base Installation

  1. Download and install Eclipse Kepler Modeling Tools.
  2. Download and unzip (login: proxy_svn, password: dW09WmzRcCUF) the file dropins.zip into your eclipse directory (your system might ask you if you want to replace the existing directory, say Yes).
  3. Download (login: proxy_svn, password: dW09WmzRcCUF) the installation helper script for your platform into your Eclipse folder: Bash Script (Linux, MAC OS X), Batch Script (Windows). On Linux and Mac, make the script executable using "chmod u+x emerge_kepler.sh".
  4. Run the script (./emerge_kepler.sh in a terminal for Linux & MAC OS X, double click or call in a command line for Windows). That takes a little while. Note that there might be some warnings about HTML cookies: do not mind.

Initial Workspace Content Check-out

  1. Start Eclipse
  2. Close the "Welcome" page if it displays
  3. Go to Window -> Preferences -> Team -> SVN (you might get an error about JavaHL: just click ok) or Eclipse -> Preferences -> Team -> SVN under Mac OS X.
  4. At the bottom of the preference page, there is an option called SVN interface: select SVN Kit.
  5. Go to File->Import->SVN->Checkout project from SVN, then create a new repository location with URL https://source.fortiss.org/svn/af3/fortiss-std-env (login: proxy_svn, password: dW09WmzRcCUF), finally select the root fortiss-std-env and click Finish.
  6. Copy the fortiss-std-env/settings/config file to your Subversion configuration (~/.subversion on Unix-like systems and %APPDATA%/Subversion/config on Windows). You may have to merge our recommendation with your setup, since there is only one global config file.
    The important section in our configuration is the auto-props section, which sets subversion properties upon adding files to the repository.
  7. Go to Window -> Preferences -> ConQAT -> Conqat Rating Support, under Excluded files (ANT pattern) hit New... and enter external-src/**
  8. Do the same with the pattern "test-src/**"
  9. Do the same with the pattern "generated-src/**"
  10. Do the same with the pattern "**/*GUI.java"
  11. Do the same with the pattern "plugin.xml"

Materializing The Target Platform And Plugin Sources, Building the Code

  1. In Eclipse, open the fortiss-std-env/buckminster folder.
  2. Double-click buckminster.target. Hit the Set as Target Platform hyperlink in the upper-right corner of the editor.
  3. Double-click af3-phoenix-kepler.cquery.
  4. Click the Resolve to Wizard button: this might take a while.
  5. After a little while, a dialog will open: click Finish (takes a while).

Starting AF3

  1. Double-click org.fortiss.af3.phoenix.product.top, then open af3_phoenix.product and select Launch an Eclipse Application
  2. On the first run, you will probably get an error The application could not start. Would you like to view the log?, press No.
  3. To fix this, go to Run->Debug configurations..., select Eclipse Application->af3_phoenix.product, go to the Plug-Ins tab and check the checkbox Workspace in the list of plugins (if not already checked).
  4. To the very right of the window (might even be hidden), press the button Add Required Plug-Ins.
  5. If running Windows 10: Due to missing support of Windows 10 in Eclipse Kepler, it is required to add the option -Dorg.osgi.framework.os.name=win32 in the text field "VM arguments" in the "Arguments" tab of the launch configuration.
  6. Press Apply and then Debug. Now AF3 will start correctly as RCP.

Install external tools

NuSMV:
To install NuSMV, download it and unzip it to a destination of your choice.
Add the path to your NuSMV executable to your PATH environment variable.

Best Practice under Mac & Linux:
  • "sudo ln -s /<your path>/NuSMV-2.5.3/NuSMV /usr/bin/NuSMV"
For Windows there are detailed descriptions if you google: change path in windows
  • add to the PATH variable "C:\...<your path>...\nusmv\bin\"
Z3:
Z3 is currently used by AF3 in two manners:
  • through command line (for some formal verification features)
  • directly through Java calls (for DSE)

To set this up, follow respectively the following instructions:

  • command line:
    • Download Z3: https://github.com/Z3Prover/bin
    • Make sure that Z3 is in the path (see corresponding instructions for NuSMV above), if yes, it should work out-of-the-box.
    • To test that Z3 is correctly installed and that AF3 correctly recognizes it, just press the "Z3 Version" button from the "Non-determinism Analyzes" View
  • Java calls:
    • On Windows: nothing to do, it should work out of the box!
    • On Linux: add the following environment variable in the run configurations of AF3:
      • Name: LD_LIBRARY_PATH
      • Value: /<path to your AF3 workspace>/com.microsoft.z3/lib/x64
    • On Mac: add the following environment variable in the run configurations of AF3:
      • Name: DYLD_LIBRARY_PATH
      • Value: /<path to your AF3 workspace>/com.microsoft.z3/lib/x64
    • In both cases above, if you are still running a 32 Bit system, eplace the x64 by x32 at the end of the path

Note that we plan on switching completely to java calls to make installation easier for the user.

FAQs

  • How to reset Eclipse Subversion credentials so Eclipse asks again next time?
    Answer: Close Eclipse if it is running. Either in a terminal or your harddisk explorer, navigate to the Eclipse installation folder (e.g. "/home/myself/eclipse/configuration/org.eclipse.core.runtime") and
    delete the ".keyring" file. This gets rid of any Subversion credentials provided to this Eclipse installation and makes it ask again next time You perform a repository action.
  • How to regenerate the parser of the grammar "AF3Expression.g"?
    Answer: In context menu of "org.fortiss.af3.expression/buckminster.cspex" perform "Buckminster->Invoke Action->generate-grammar".
  • What Eclipse VM arguments should be used?
    Answer: -Xmx1024m -Xss32m. See also Issue #269 if you are on Windows regarding reduced stack size.
  • My Eclipse installation constantly crashes!
    Answer: This is propably due to a known bug(https://bugs.openjdk.java.net/browse/JDK-8154831) that is fixed in JDK8u111/u112 and above. Please update your Eclipse installation. For older versions, adding the line -XX:CompileCommand=exclude,org.eclipse.jdt.internal.compiler.parser.TypeConverter::* to the eclipse.ini file which is located in the folder where eclipse kepler has been extracted to can be used as a workaround.
  • When trying to Resolve to Wizard Buckminster tells me "No suitable provider for component xxx" (lucene, swtbot, hamcrest, mortbay, org.apache.commons.el, org.eclipse.update.core.win32, ...)
    Answer: Please try to apply one of the following fixes. In any case, please report the issue so the problem can be corrected.
    • Try to fix the provider URL in the fortiss-std-env/buckminster/.rmap file corresponding to your Eclipse version (fortiss_kepler.rmap for Eclipse Kepler). E.g., for orbit, a more recent snapshot can be found here: http://download.eclipse.org/tools/orbit/downloads/.
    • Alternatively, you can try to manually install the missing package. E.g., in the case of missing swtbot go to Help -> Install new Software..., insert http://download.eclipse.org/technology/swtbot/releases/latest/, press Select All and hit Finish.
    • As a last resort, get an AF3 distribution, go to the /plugins folder, search for the missing .jars and add them to the fortiss-std-env/target-platform folder in your workspace. After that restart Eclipse and retry Resolve to Wizard.
  • Menu icons are not displayed on KDE.
    Answer:
    • Go to "Systemsettings - Application Style - GNOME Application Style".
    • Select "Show symbols of GTK buttons".
    • Select "Show symbols in GTK menus".