Skip to content

How To Use

Jump to bottom
Luis Diogo Couto edited this page Feb 2, 2016 · 16 revisions

This guide provides instructions for building a new Tempo UI. Refer to the example folder in the main repo to follow along.

This guide assumes basic knowledge of DukeScript and the Remote Control feature described in Section 15.2 of the Overture User Guide.

Step 0: Bootstrap

A TempoUI is essentially a DukeScript project with some additional code to extend the bindings towards VDM. Speaking of which, the DukeScript documentation is a valuable resource for TempoUIs.

To create an initial UI project, we use Maven archetypes (see https://github.com/dukescript/maven-archetypes):

mvn archetype:generate 
    -DarchetypeGroupId=com.dukescript.archetype
    -DarchetypeArtifactId=knockout4j-archetype 
    -DarchetypeVersion=0.9

This will create a root folder for your project with 2 modules: client and js. We ignore js. You can rename the modules however but we will leave them as is. The client model will some demo code from the DukeScript archetype. You can either use it as a starting point or delete it.

Now, add TempoUI as a dependency to the client/pom.xml:

<dependency>
  <groupId>org.overturetool</groupId>
  <artifactId>tempoui</artifactId>
  <version>1.0-SNAPSHOT</version>
</dependency>

At this point, you should be able to mvn compile.

Step 1: Building the Model API

The first step of actual UI development is building an API for the UI to interact with the model. The role of the Model API is to expose model functionality to the UI. We can provide an API for an existing model or define the API upfront and develop the model later. The latter option works well when developing the UI and model in parallel, provided everyone agrees on the API.

The ModelAPI (or whatever else we want to call it) is a handwritten mostly static Java class that exposes the VDM model operations that we want to trigger from the UI. This class is handwritten for two reasons:

  • we only want to expose a subset of operation
  • we may need to do encoding values from the UI into VDM values

In the future, we would like to generate this class from a configuration and automate the encoding. But for now, it's manual. To expose a VDM operation named foo, use something like:

public static void foo(RemoteInterpreter ri) throws Exception {
  interpreter.execute(ROOT_NAME + ".bar()");
}

As you can see, the ModelAPI and VDM names don't have to match. Also, the ModelAPI methods are all static and the class itself has a static reference to the interpreter that is being controlled with the UI. The methods must be static in order to be accessed from the UI. The interpreter reference is needed to execute the VDM operations.

The VDM model itself has no static class restrictions but we will need to store the names of any VDM objects we want to call operations on. The easiest thing to do is to only cal operations on the top-level VDM object -- what roughly corresponds to the entry point. The name of this object can then be easily stored in a constant. Also, remember that there is no checking on the VDM strings that we submit to the interpreter so be careful.

Step 2: Building the UI Data Model

Once we have the ModelAPI in place, we can build the Data Model for the UI. This is a Java class that DukeScript binds to the UI using the Knockout library. This class is typically called DataModel but should never be confused with the VDM model. We'll refer to it as UiDataModel to help disambiguate.

The UiDataModel is defined through annotations and code generation provided by DukeScript. When defining the UiDataModel, we need to use operations from the ModelAPI and also declare properties to hold any VDM variables that we want to bind to the UI.

For example, the following snippet defines a basic UiDataModel with a single property (ok).

@Model(className = "VdmData", targetId="",properties = {
        @Property(name = "ok", type = boolean.class),
})
final class UiModelData {
}

In order to expose methods, we use the @Function annotation. The annotated method must be static. The generated data class (VdmData) is always passed as a parameter

@Function
static void foo(VdmData vdm) throws Exception {
  ModelAPI.foo();
}

For more about Data Models see https://dukescript.com/getting_started.html.

Step 3: Binding the HTML5 UI

Tempo UIs are built with HTML5 and JavaScript. We will not discuss how to build the UI except to say that we can use any standard HTML5 technology when building the UI. In addition, the UI can be designed and developed independently from the model.

For connecting the UI to model, the Maven archetype will have created a file src/main/webapp/pages/index.html. This is the page that is loaded in the browser when the model is launched (see Step 5). The UI must start from this page.

The HTML5 UI elements are bound to the UiDataModel properties using Knowckout. Refer to the Knockout documentation (http://knockoutjs.com/documentation/introduction.html) for information on what kinds of bindings are available.

As an example, here is a trivial HTML snippet that binds a status message to the ok property:

<p>
  Status is: <em data-bind="if: ok"style="color:green">Ok</em>  <em data-bind="if: !ok"style="color:red">Not Ok</em>
</p>

Step 4: Building the Remote Controller

In regular DukeScript applications, the application logic is a "plain" Java application. In the TempoUI, the application log is a VDM Model wrapped in a Remote Control class, as described in section 15.2 of the Overture user guide.

A Remote Controller for a TempoUI is similar to any other Remote Control class but it has a few caveats. TempoUI provides a starting controller --TempoRemoteControl -- that we can subclass. This class takes care of loading the interpreter and launching the browser-based UI.

This class is also responsible for connecting the connecting the VDM Model and the `UiDataModel. This must be done in a static method.

Therefore, to build a Remote Controller for a UI, we subclass TempoRemoteControl and implement a public static void method called onPageLoad(). This method handles the final stages of connecting the UI to the the VDM model.

Broadly speaking, onPageLoad must do the following:

  • initialise the UiDataModel
  • acquire a reference to the root (or top-level) value of the VDM model from the interpreter
  • construct a list of model variables to be monitor
  • attach listeners to those variables (TempoUI provides a class that does this).

The snippet below shows a sample method.

public static void onPageLoad() throws Exception {
  // Create  UiDataModel and bind it to the UI
  VdmData uiData = new VdmData();
  uiData.applyBindings();

  // Acquire top-level value
  String root = "foo";
  String rootConstructor = "new Foo()";
  interpreter.create(root, rootConstructor);
  Value v = interpreter.valueExecute(root);
 
  // Create list of VDM variables to bind
  List<ListenerAttacher.VarBindInfo> vars = new ArrayList<>(1);
  vars.add(ListenerAttacher.VarBindInfo.create("ok", new ABooleanBasicType()));

  // Attach listener to notify UiDataModel of variable changes
  ListenerAttacher la = new ListenerAttacher(v, vars, uiData);
  la.apply();
}

Step 5: Launching

Launching TempoUIs is very simple. Simply launch the VDM model with a remote control class. This can be done in the Overture IDE or the command line (it should also work for VDMJ but that is not officially supported). The remote control class is the one we have built in Step 4.

The UI we showed in Step 3 would like this:

Final tip: It's possible to launch and debug the remote controlled model from within a Java IDE by running the overture interpreter project (main class org.interpreter.VDMJ) with the following arguments: -vdm[sl|pp|rt] -i /path/to/model/sources -remote fully.qualified.RemoteControlClass. You must also set the UI project as a dependency of the interpreter. This has been tested with Eclipse and IntelliJ but should work with others IDEs.

Clone this wiki locally