Configuring JJTree in Android Studio

First, follow the steps described in Configuring JavaCC in Android Studio.
Next, modify the module's build.gradle file as shown below:

android {
    // ...
    sourceSets {
        main {
            java.srcDirs = ['src/main/java',
                            file(project.buildDir.absolutePath + '/generated/jjtree'),
                            file(project.buildDir.absolutePath + '/generated/javacc')]
        }
    }
    applicationVariants.all { variant ->
        variant.javaCompile.dependsOn.add(compileJavacc)
    }
    // ...
}

compileJavacc {
    inputDirectory = file(project.buildDir.absolutePath + '/generated/jjtree')
    dependsOn.add(compileJjtree)
}

Move you *.jj file from src/main/javacc, which is JavaCC default directory, to src/main/jjtree, and change its extension to *.jjt.  When you build your project now, everything should continue to work, including all JavaCC unit tests.  In addition, you'll find new JJTree files under build/generated/jjtree.

You can also setup a task that cleans generated JavaCC and JJTree files, and make compileJavacc task depend on it:

task cleanJjdirs(type: Delete) {
    delete file(project.buildDir.absolutePath + '/generated/jjtree'),
            file(project.buildDir.absolutePath + '/generated/javacc')
}

Fixing Semantic LOOKAHEAD sample

Semantic LOOKAHEAD sample incorrectly states that the BC() choice must be made only when the next token is a "c", and the token following that is not a "c".  It actually should say that the BC() choice must be made only when the next token and the following tokens are “c”. To make the sample work the production should look like this:

void BC() :
{}
{
  "b"
  [ LOOKAHEAD( { getToken(1).kind == C && getToken(2).kind == C } )
    <C:"c">
  ]
}

The semantic lookahead is not really required here; the production can be simplified by using syntactic lookahead:

void BC() :
{}
{
  "b" [ LOOKAHEAD( "c" "c" ) "c" ]
}

Configuring JavaCC in Android Studio

Apply JavaCC plugin for Gradle.  The top-level build.gradle should look something like this:

buildscript {
    repositories {
        jcenter()
    }
    dependencies {
        classpath 'com.android.tools.build:gradle:2.0.0-alpha3'
        classpath 'ca.coglinc:javacc-gradle-plugin:2.3.1'  
    }
}

Apply the plug-in in the module's build.gradle file:

apply plugin: 'com.android.application'
apply plugin: 'ca.coglinc.javacc'

Make your Java compilation tasks depend on compileJavacc task and add Java files generated by Javacc to your source path:

android {
    // ...
    sourceSets {
        main {
            java.srcDir compileJavacc.outputDirectory
        }
    }
    applicationVariants.all { variant ->
        variant.javaCompile.dependsOn compileJavacc
    }
    // ...
}

When integrating into an Android library, replace applicationVariants with libraryVariants.

Finally, install JavaCC IntelliJ plug-in to enable syntax highlighting.

Optimized PrintT is now in the latest Toolbox daily build

The latest Toolbox daily build can be found here.  It removes most significant bottlenecks in handling large amount of TLC output (e.g., PrintT in TLC module).

Another notable change is a new modules node under the open spec node which lists all dependent modules.  This makes exploring dependencies much easier.  It also has "Quick Access..." menu item under Windows which also lists all dependent modules and the spec's models.

Selecting a sub-sequence

The standard Sequences module defines SelectSeq operator which provides a convenient way of selecting sequence elements that satisfy some condition.  However, when working with sequences, it is more practical to select a set of indices of the elements instead of elements themselves.  Having a set of indices, selected by SelectIdx operator, allows easily modify the original sequence, as shown below.

Composing TLA+ specs from modules

Suppose we have a system consisting a Client, a Device, and a Server. The Client talks to the Device, the Device communicates with the Server.   Naturally, we would have 3 TLA+ modules, one for each system component.

What's the best way to compose the modules into a final spec?

One way is to instantiate the Device from the Client module, and the Server from the Device module.  But TLC model checker does not deal with existential quantifiers of temporal logic:  the Device would have to accept the Server's variables as parameters so that it could pass them to the Server when instantiating the Server module.   It means the Device would have to declare variables that it does not use.

In reality, the Device does not need to know about the Server.  All it needs to know about is communication channels between the Client and the Server.  We can instantiate both the Device and the Server in the Client module, as shown below.  In this case the Device does not need to declare Server's variables and accept them as parameters.  This makes the spec cleaner.  As a bonus, Next step action reminds us at the top level which variables are not used by the Device and by the Server.

From practical point, a module's interface consists of constants and variables that it accepts as parameters,  TypeInvariant operator, and the Next step action.  In even cleaner approach, we could create a Test module and declare all the required variables there.  Then we could instantiate Client, Device, and Server modules from Test module, passing the required parameters.  Then we could compose Test's TypeInvariant and Next step action using the instantiated modules.  When modules are independent of each other, it is easier to test each module separately as described in this post.

Test your specs!

A practical advice: when specifying a large system, use modules and TLA+ support for module instantiation.  Split the system into logical components, map each component to a TLA+ module.  Create a test module for each component module.  Instantiate a component module within a test module. Create a model and run it to test the instantiated component module.

This helps a lot with finding specification bugs early in the process.

At the very minimum test type invariants. Test modules do not need to be complicated, just something simple like shown below.

Reducing number of fields in a record set

The TLA+ definition of records as functions makes it possible to manipulate records in ways that have no counterparts in programming languages.  For example, we can define an operator S such that S(r, s) is a record obtained from r by removing each field that is also a field of the record s:

S(r, s) == [ x \in (DOMAIN r \ DOMAIN s) |-> r[x] ]

Now, if we have a set of records defined as

Rec1 == [a : Nat, b : Nat, c : Nat, d : Nat]

we then can define another set of records that have all fields of records in the set Rec1, except the field b, as

Rec2 == { S(r, [b |-> {}]) : r \in Rec1 }

This is quite handy when records in Rec1 have many fields.

Adding new CHOOSE constructs and TLC model checker

After adding new operator that uses CHOOSE, like

NullData == CHOOSE x : x \notin Data

TLC Model Checker may report type invariant violations in existing models.  The problem is that TLC Model Checker does not pick up new NullData operator.  To fix the problem,  NullData  needs to be added by hand to Definition Overrides with Model Value set as NullData's value.

Unlocking Nexus 9

Unlocking Nexus 9 is simple - just follow the instructions from Factory Images for Nexus Devices.  The only precondition is Settings -> Developer Settings -> OEM unlocking should be enabled (checked).  Otherwise fastboot oem unlock will fail.