Skip to content

SpecCompiler

Jump to bottom
Cameron Finucane edited this page Jul 2, 2013 · 10 revisions

SpecCompiler handles everything necessary to turn a specification and map into a strategy (if possible).

Broadly, this operation can be split into two steps: Parsing (Specification + Map → Synthesizer Input Files) and Synthesis (Synthesizer Input Files → Strategy).

Parsing

Overview

SpecCompiler takes as input a task specification and either a map of the physical workspace or an abstract description of the workspace topology. Note that if a map is used, extra pre-processing is performed on it before parsing (see Map Processing).

SpecCompiler: Parsing Overview

Map Processing

If a map is used, in addition to several optional steps (described below), topological adjacency information must be extracted from the map.

SpecCompiler: Map Processing Overview

Details

  • Locative phrase substitution: Detect any non-projective prepositional phrases (e.g. "between r1 and r2") in the specification, create a new region in the map that corresponds to this location (in this case, ConvexHull(r1 ∪ r2)\(r1 ∪ r2)), and substitute the phrase with a reference to the name of the new region (e.g. "_between_r1_and_r2"). For more information, see Map Processing.

  • Specification Parser: Takes a specification and a list of proposition names (regions, sensors, actuators, etc.) and creates an equivalent LTL specification. See Parsers for more information.

  • Overlapping region resolution: Splits up any overlapping regions. For example: consider a map of only "r1" and "r2", which partially overlap. These regions would be replaced by [r1\r2, r1 ∩ r2, r2\r1]. For more information, see Map Processing.

  • Convex decomposition algorithm: Break up any concave regions into convex subregions (using the MP5 algorithm). This is only necessary for motion control handlers that require convex regions. For more information, see Map Processing.

  • Topological adjacency calculation: For each region, determine which other regions can be reached from it directly. Currently, this assumes topological adjacency if and only if two regions have at least one face (or subface) in common. (TODO: How to add in dynamics-based calculations?)

  • Decomposed region name substitution: Map Processing will output a map with regions named "p1", "p2", etc. This step modifies the specification to refer to these subregion names (so that the specification correctly corresponds with the updated abstraction). Note: (1) This is done after, instead of before, parsing the specification because—among other reasons— it introduces parentheses into the specification. (2) To map these subregion names back to the human-readable name of their original parent region, see getAnnotatedRegionName() (TODO: fix reference)

  • Topological constraint addition: Add LTL corresponding to the topological constraints to the system requirements portion of the specification

  • Bit-vector encoding: Since the robot cannot be in more than one region at any time, we can reduce the total number of propositions used (from N to ceil(log_2(N))) by encoding regions into a bit-vector ("bit0", "bit1", etc.). This step takes care of that substitution. Note: To map back from bit-vector representations to the corresponding region object, see regionFromState() (TODO: fix reference)

  • Macro substitution: Some statements such as "stay there" are much easier to implement outside of the parser. Therefore, the parser can pass on macros like STAY_THERE to be post-processed by this later step. For more information, see [Specification Macros](Specification Macros).

  • Synthesizer input file creation: Outputs the specification in a file format appropriate for the synthesizer that will be used in the next step.

Configuration

Relevant CompileOptions in the .spec file (set to True to enable and False to disable):

  • parse_locative_phrases (Locative phrase substitution)
  • split_overlapping_regions (Overlapping region resolution)
  • convexify (Convex decomposition)
  • use_region_bit_encoding (Bit-vector encoding; also affects output of macro substitution)
  • parser (Parser type) As of now, supported options are:
    • structured ([Structured English](Structured English Parser))
    • slurp (SLURP)
    • ltl ([Raw LTL](Raw LTL Specification Parser))

(Note: Decomposed region name substitution will effectively be a no-op if the first three of the above are all set to False)

Synthesis

Overview

Synthesis produces a correct-by-construction discrete controller from a LTL specification. (Unless the specification is unrealizable.)

LTLMoP currently supports two synthesis tools:

  • JTLV-GROne, written in Java using the JTLV framework. (Default)
  • slugs, written in C++ (Beta)

Configuration

Relevant CompileOptions in the .spec file (set to True to enable and False to disable):

  • fastslow (Use fast/slow semantics, for both synthesis and execution)
  • explicit_strategy (Export the strategy as an explicit automaton, instead of a more-compact BDD)

Input Files

  • JTLV-GROne takes a .smv file, listing the names of propositions and to which player each belongs, as well a .ltl file containing the specification.

  • slugs has its own input file format (.slugsin) which contains both proposition names/players and a RPN-formatted specification, but a script is included in its distribution to convert JTLV-GROne input to slugs format (if you are using LTLMoP, though, you do not need to worry about this).

Output Files

The synthesis tools can export the strategy as either an explicit-state automaton (.aut file) or a BDD (.bdd file). These should function equivalently; the BDD is generally more compact, but for some applications an explicit-state strategy is easier to manipulate.

Clone this wiki locally