SpecEditor - VerifiableRobotics/LTLMoP GitHub Wiki

The specification editor (specEditor.py) is where the user specifies a mission for the robot, by dictating tasks in one of the supported languages. It consists of three windows and the menu bar, as shown below and explained in depth in the remainder of this page:

 * Main window: This is where the user actually types in the specification tasks (components of the robot's mission) * Right window: Propositions (Regions - Sensors - Actions - Custom) * Bottom window: Compiler Log - LTL Output - Workspace Decomposition * Menu bar: File - Edit - Run - Debug

For theoretical background information, please see this paper.

For detailed instructions on how to create a map, write a specification, and run (simulate) the mission, please see the tutorial.

The user can describe the robot's mission by typing individual tasks in separate lines of the editor. The three supported languages are mentioned below. This wiki page will focus on [Structured English](Structured English Parser), which is the default language.

When typing a specification, commands are not case-sensitive, with the exception of propositions. If a proposition name is spelled correctly, with respect to how it is defined in the Right Window, the text will turn blue. For example, gO TO room1 is OK, but go to Room1 will result in the following error: ERROR(4): Could not parse the sentence in line 1 because Room1 is not recognized when compiling the specification.

Finally, to comment a line out, insert a # at the beginning of the line. The text will turn green.

 #### Supported Language Pipelines The user can choose to write [task specifications](Task Specifications) in any of the following languages: * [Structured English](Structured English Parser) (`default`) * A small subset of natural language via [SLURP](SLURP) (Situation and Language Understanding Robot Platform) * [Raw LTL](Raw LTL Specification Parser) (specifically, the [GR(1) fragment](http://laser.inf.ethz.ch/2005/reports/react.pdf) of Linear Temporal Logic)

The choice is made in the Parser mode menu, as shown below:

 ### Right window ### The right window is split into four sections, one for each type of proposition that can be defined.

In order to control a physical robot, the abstract sensors and actions defined below should be mapped to actual sensors and actuators via the ConfigEditor. This step is not necessary when running simulations.

Regions are robot propositions that refer to parts of the robot's workspace. A workspace is created using the Region Editor.


Sensors are propositions whose value is controlled by the environment. They are abstractions of the physical sensors, in the sense that their value is either true or false. For example, the doorClosed sensor is `false' when the door it's referring to is open.


Actions are propositions whose value is controlled by the robot. They are also abstractions of the physical sensors, in the sense that their value is either true or false, depending on whether the corresponding actuator is activated or not. For example, the robot can activate the dance action as part of its mission.


Custom propositions are robot propositions as well, but they do not correspond to some physical action that the robot can perform.

The bottom window is populated once the user compiles the specification via the Run menu, as show below:


The compiler log informs the user about the result of the compilation process. In the screenshot below, the specification was realizable, and a winning strategy was computed.

 If the specification was changed to: ``` robot starts in room1 go to room2 always not room2 ``` the compiler log would report an error, because lines 2 and 3 of the specification contradict each other. LTLMoP has an [analysis tool](#Analysis) that helps the user debug the specification.  Note the warning that appears in the first section of the compiler log, due to the fact that some propositions have been defined in the Right Window, but have not been used in the specification: ``` Warning: The following propositions seem to be unused: ['e.alarm', 'e.doorClosed', 's.dance'] They should be removed from the proposition lists ```

The LTL equivalent of the Structured English specification is diplayed in this tab of the Bottom Window. An explanation of the symbols that appear can be found [here](Raw LTL Specification Parser).

 #### Workspace Decomposition By default, LTLMoP will break up any concave regions into convex subregions (using the MP5 algorithm). This is only necessary for [motion control handlers](Handlers#motion-control) that require convex regions. For more information, see [Map Processing](Map-Processing#convex-decomposition-algorithm). The resulting decomposed workspace is displayed in this tab of the bottom window. 

The File menu can be used to:

• Create a New specification file.
• Open an existing file, such as one of the [examples](Existing Examples).
• Import an existing workspace map.
• Close/Save the current file.


The Edit menu has standard functions that facilitate the writing of specification tasks.


The Run menu is used to Compile the specification and then Simulate the mission, given that the compilation (synthesis) process was successful. There are also various Compilation options:

• Workspace Decomposition
• Fast-Slow Synthesis
• Bit-vector Encoding
• Parser mode

Finally, the Configure Simulation... button opens the ConfigEditor.


The Debug menu provides analysis tools to debug unsynthesizable specifications.