RFC-010: Implementation of Transition Exploration Server

Table of Contents

• RFC-010: Implementation of Transition Exploration Server
• Problem
• Proposal
  • Overview
  • Requirements
  • Architecture
  • API
  • Constructing the IR
  • Protocol
    • gRPC Example

Problem

Users of Apalache have voiced a need for the following kinds of behavior:

• incremental results (that can be iterated through to exhaustively enumerate all counterexamples)
• interactive selection of checking strategies
• interactive selection of parameter values

The discussion around these needs is summarized and linked in #79 .

The proximal use cases motivating this feature are discovered in the needs of or collaborators working on implementing model based testing (MBT) via the Modelator project. @konnov has given the following articulation of the general concern:

For MBT we need some way to exhaustively enumerate all counterexamples according to some strategy. There could be different strategies that vary in terms of implementation complexity or the number of produced counterexamples

The upshot: we can provide value by adding a utility that will allow users to interactively and incrementally explore the transition systems defined by a given TLA+ spec.

Proposal

Overview

In the current architecture, there is a single mode of operation in which

• the user invokes Apalache with an initial configuration, including an input specification,
• the specification and configurations are parsed and pre-processed,
• and then the model checker proper drives the TransitionExecutor to effect symbolic executions verifying the specified properties for the specified model.

This RFC proposes the addition of a symbolic transition exploration server. The server will allow a client to interact with the various steps of the verification process. The client is thus empowered to call upon the parser and preprocessors at will, and to drive the TransitionExecutor interactively, via a simplified API.

The specific functionality that should be available for interaction is enumerated in the Requirements.

As per previous discussions, interactivity will be supported by running a daemon (or "service") that serves incoming requests. Clients will interact via a simple, well supported protocol, that provides an online RPC interface.

As a followup, we can create our own front-end clients to interact with this server. In the near term, we envision a CLI, a web front-end, and editor integrations. Many aspects of such clients should be trivial, once we can use the client code generated by the gRPC library . See the gRPC Example for details.

Requirements

The following requirements have been gathered through conversation and discussion on our GitHub issues:

| TRANS-EX.1::QCHECK.1 | : enable checking specs without repeated JVM startup costs 730#issue-855835332

| TRANS-EX.1::EXPLORE.1 | : enable exploring model checking results for a spec without repeated preprocessing costs 730#issue-855835332

| TRANS-EX.1::LOAD.1 | : enable loading and unloading specs 730#issuecomment-818201654

| TRANS-EX.1::EXTENSIBLE.1 | : The transition explorer should be extensible in the following ways:

| TRANS-EX.1::EXTENSIBLE.1::CLOUD.1 | : extensible for cloud-based usage

| TRANS-EX.1::EXTENSIBLE.1::CLI.1 | : extensible for interactive terminal usage |

| TRANS-EX.1::SBMC.1 | : expose symbolic model checking 730#issue-855835332

| TRANS-EX.1::SBMC.1::ADVANCE.1 | : can incrementally advance symbolic states

| TRANS-EX.1::SBMC.1::ROLLBACK.1 | : can incrementally rollback symbolic states

| TRANS-EX.1::SBMC.1::TRANSITIONS.1 | : can send data on available transitions

| TRANS-EX.1::SBMC.1::SELECT.1 | : can execute a specific transition given a selected action

| TRANS-EX.1::SBMC.1::COUNTER.1 | : supports enumerating counterexamples 79#issue-534407916

| TRANS-EX.1::SBMC.1::PARAMS.1 | : supports enumerating parameter values (CONSTANTS) that lead to a counterexample 79#issuecomment-576449107

Architecture

The interactive mode will take advantage of the TransitionExecutor's abstraction for writing different model checking strategies, to give the user an abstracted, interactive interface for dynamically specifying checking strategies.

I propose the following high-level architecture:

• Use an RPC protocol to allow the client and server mutually transparent interaction. (This allows us to abstract away the communication protocol and only consider the functional API in what follows.)
• Introduce a new module, ServerModule, into the apa-tool package. This module will abstract over the relevant BMC passes which lead up to, and provide input for, the TransitionExplorer, described below.
• Introduce a new module, TransitionExplorer that enables the interactive exploration of the transition system.
• Internally, the TransitionExplorer will make use of the TransitionExecutor and relevant aspects of the SeqModelChecker (or slightly altered versions of its methods).

NOTE: The high-level sketch above assumes the new code organization proposed in ADR 7.

API

The following is a rough sketch of the proposed API for the transition explorer. It aims to present a highly abstracted interface, but in terms of existing data structures. Naturally, refinements and alterations are to be expected during implementation.

We refer to symbolic states as Frames, which are understood as a set of constraints, and we put this terminology in the API in order to help users understand when they should be thinking in terms of constraint sets as opposed to concrete states. Concrete states can be obtained by the functions suffixed with Example.

In essence, this proposed API is only a thin wrapper around the TransitionExecutor class. During previous iterations of the proposed API we discussed exposing a higher-level API, targeted at meeting the requirements more directly. However, discussion revealed that the expensive computational costs of SAT solving in most cases made it infeasible to meet the requirements in this way. Instead, we must expose most of the underlying logic of the TransitionExecutor, and task the users with building their own exploration strategies with these primitives.

It is likely that we will be able to provide some higher-level functionality to users by way of wrapper libraries we implement on top of the proposed API, but that work should be left to a subsequent iteration.

NOTE: This interface is intended as an abstract API, to communicate the mappings from request to reply. See the gRPC Example for a sketch of what the actual implementation may look like.

/** A State is a map from variable names to values, and represents a concrete state.  */
type State = Map[String, TlaEx]

/** An abstract representation of a transition.
 *
 * These correspond to the numbered transitions that the `TransitionExectur` uses
 * to advance frames. But we likely want to present some more illuminating metadata
 * associated with the transitions to the users. E.g., ability to view a
 * representation as a `TlaEx` or see an associated operator name (if any)?  */
type Transition

/** An execution is an alternating sequence of states and transitions,
 *  terminating in a state with no transition.
 *
 * It is a high-level representation of the `EncodedExecution` maintained by the
 * transition executor).
 *
 * E.g., an execution from `s1` to `sn` with transitions `ti` for each `i` in `1..n-1`:
 * 
 *     List((s1, Some(t1)), (s2, Some(t2)), ..., (sn, None))
 */
type Execution = List[(State, Option[Transition])]

trait UninitializedModel = {
  val spec: TlaModule
  val transitions: List(Transition)
}

trait InitializedModel extends UninitializedModel {
  val constInitPrimed: Map[String, TlaEx]
}

/** An abstract representation of the `CheckerInput`
 *
 * A `Model` includes all static data representing a model.
 * 
 * An `UninitializedModel` is missing the information that would be needed in
 * order to actually explore its symbolic states (such as the initial values of
 * its constants).
 *
 * An `InitializedModel` has all data needed to explore its symbolic states. */
type Model = Either[UninitializedModel, InitializedModel]

/**  The type of errors that can result from failures when loading a spec. */
type LoadErr

/**  The type of errors that can result from failures to assert a constraint. */
type AssertErr

/**  The type of errors that can result from checking satisfiability of a frame. */
type SatError

/**  Maintains session and connection information */
type Connection

trait TransEx {

  /** Used internally */
  private def connection(): Connection

  /** Reset the state of the explorer
   *
   * Returns the explorer to the same state as when the currently loaded model
   * was freshly loaded. Used to restart exploration from a clean slate.
   *
   * [TRANS-EX.1::LOAD.1]
   */
  def reset(): Unit

  /** Load a model for exploration
   *
   * If a model is already loaded, it will be replaced and the state of the exploration
   * [[reset]].
   *
   * [TRANS-EX.1::QCHECK.1]
   * [TRANS-EX.1::LOAD.1]
   * [TRANS-EX.1::SBMC.1::TRANSITIONS.1]
   * 
   * @param spec the root TLA+ module 
   * @param aux auxiliary modules that may be required by the root module
   * @return `Left(LoadErr)` if parsing or loading the model from `spec` goes
   *          wrong, or `Right(UninitializedModel)` if the model is loaded successfully.
   */
  def loadModel(spec: String, aux: List[String] = List()): Either[LoadErr, UninitializedModel]

  /** Initialize the constants of a model
   *
   * This will always also reset an exploration back to its initial frame. */
  def initializeConstants(constants: Map[String, TlaEx]): Either[AssertErr, InitializedModel]

  /** Prepare the loaded modle with the given `transition` */
  def prepareTransition(transition: Transition): Either[AssertErr, Unit]

  /** The transitions that have been prepared. */
  def preparedTransitions(): Set[Transition]

  /** Apply a (previously prepared) transition to the current frame.
   *
   * Without any arguments, a previously prepared transition is selected
   * nondeterministically.
   *
   * When given a `transition`, apply it if it is already prepared, or prepare
   * it and then apply it, if not.
   * 
   * Interfaces to `assumeTransition` and `pickTransition`, followed by
   * `nextState`. */
  def applyTransition(): Either[AssertErr, Unit]
  def applyTransition(transition: Transition): Either[AssertErr, Unit]

  /** Assert a constraint into the current frame
   *
   *  Interface to `assertState` */
  def assert(assertion: TlaEx): Either[AssertErr, Unit]

  /** The example of an execution from the an initial state up to the current symbolic state
   *
   * Additional executions can be onbtained by asserting constraints that alter the
   * search space. */
  def execution: Either[SatErr, Execution]

  /**
   * Check, whether the current context of the symbolic execution is satisfiable.
   *
   * @return Right(true), if the context is satisfiable;
   *         Right(false), if the context is unsatisfiable;
   *         Left(SatErr) inidicating if the solver timed out or reported *unknown*.
   */
  def sat(): Either[SatErr, Boolean]

  /** Terminate the session. */
  def terminate(): Unit
}

object TransEx {
  /**  Create a transition explorer
   *
   * Establishes the connection and a running session
   *
   * The channel is managed by the gRPC framework. */
  def apply(channel: Channel): TransEx = ...
}

Constructing the IR

In order to form assertions (represented in the spec as values of TlaEx), users will need a way of constructing the Apalache IR. Similarly, they'll need a way of deconstructing and inspecting the IR in order to extract useful content from the transitions.

To meet this need, the gRPC libraries we generate for client code will also include ASTs in the client language along with generated serialization and deserialization of JSON represents into and out of the AST. This will enable users to construct and inspect expressions as needed.

Protocol

We have briefly discussed the following options:

• Custom protocol on top of HTTP
• JSON-rpc
• gRPC

I propose use of gRPC for the following reasons:

• It will automate most of the IO and protocol plumbing we'd otherwise have to do ourselves.
• It is battle tested by industry
• It is already used in Rust projects within Informal Systems. This should make it easier to integrate into modelator.
• The Scala library appears to be well documented and actively maintained.
• Official support is provided in many popular languages, and we can expect well-maintained library support in most languages.
• The gRPC libraries include both the RPC protocol and plumbing for the transport layer, and these are decomposable, in case we end up wanting to use different transport (i.e., sockets) or a different protocol for some purpose down the line.

For a discussion of some comparison between JSON-rpc and gRPC, see

• https://www.mertech.com/blog/know-your-api-protocols
• https://stackoverflow.com/questions/58767467/what-the-difference-between-json-rpc-with-http2-vs-grpc

I have asked internally, and engineers on both tendermint-rs and hermes have vouched for the ease of use and reliability of gRPC.

Using gRPC can help satisfy [TRANS-EX.1::EXTENSIBLE.1] in the following ways:

• [TRANS-EX.1::EXTENSIBLE.1::CLOUD.1] should be satisfied out of the box, since HTTP is the default transport for gRPC.
• [TRANS-EX.1::EXTENSIBLE.1::CLI.1] can be satisfied by implementing a CLI client that we can launch via an Apalache subcommand.

gRPC Example

Here is as simple example of what it would actually look like to configure gRPC for the server (adapted from ScalaPB grpc):

We define our messages in a proto file:

syntax = "proto3";

package com.trans-ex.protos;

service TransExServer {
        rpc LoadModel (LoadRequest) returns (LoadReply) {}
}

message LoadRequest {
  required string spec = 1;
  optional repeated string aux = 2;
}

message LoadReply {
  enum Result {
    OK = 0;
    PARSE_ERROR = 1;
    TYPE_ERROR = 2;
    // etc...
  };
  
  required Result result;
  required Model model;
}

The generated Scala will look roughly as follows:

object TransExGrpc {
  // Abstract class for server
  trait TransEx extends AbstractService {
    def serviceCompanion = TransEx
    def loadModel(request: LoadRequest): Future[LoadReply]
  }

  // Abstract class for block client
  trait TransExBlockingClient {
    def serviceCompanion = TransEx
    def loadModel(request: LoadRequest): LoadReply
  }

  // Abstract classes for asynch client + various other boilerplate
}

A sketch of implementing a server using the gRPC interface:

class TransExImpl extends TransExGrpc.Greeter {
  override def loadModel(req: LoadRequest) = {
    val rootModule = req.model
    val auxModules = req.aux
    
    // run incomming specs through parsing passes
    val model : UninitializedModel = Helper.loadModel(rootModule, auxModules)
    
    val reply = LoadReply(result = Ok, model = model)
    Future.successful(reply)
  }
}

A sketch of using the client (e.g., to implement our CLI client):

// Create a channel
val channel = ManagedChannelBuilder.forAddress(host, port).usePlaintext(true).build
// Make a blocking call
val request = LoadRequest(spec = <loaded module as string>)
val blockingStub = TransExGrpc.blockingStub(channel)
val reply: LoadReply = blockingStub.loadModel(request)

reply.result match {
  ParseError => // ...
  Ok =>
    val model: UninitializedModel = reply.model
    // ...
}

NOTE: To ensure that we are able to maintain a stable API, we should version the API from the start.