LTS+

PLEASE NOTE: This extension requires Java in order to work. Please make sure you have Java installed and available to use on the command (You can check this by running java -version)

This extension provides rich support for writing Labelled Transition Systems (LTS) using FSP specifications.

Features

• [x] Parse, Compile & Compose LTS Files
• [x] Check safety, progress and liveness properties
• [x] Syntax Highlighting (Available via this extension for now. We are working on our own implementation)
• [ ] Intellisense or Code Autocompletion
• [x] Custom Output Console (Switched to VSCode's console output)
• [x] Custom Graph Console to view models (Switched to d3-graphviz displayed using VSCode's Webview API)

Installation

To install the extension, please follow the following steps:

1. Install Java on your machine
2. Install VSCode on your machine
3. In VSCode, go to the extensions tab (or press Ctrl + Shift + X or Cmd + Shift + X)
4. Search for "ltsp", select the first result and click install

Usage

Using the extension is straightforward. Install the extension, open an LTS file (we recommend this extension for Syntax Highlighting), open the command palette (Shortcut: Ctrl/Cmd + Shift + P) and type one of the following commands to do the associated action:

• LTS+: Build.Parse
• LTS+: Build.Compile
• LTS+: Build.Compose
• LTS+: Check.Safety
• LTS+: Check.Progress
• LTS+: Check.LTL_Property

This will open an a new window in VSCode with different output tabs. Here's a visual demo of how that works and how to use the graph visualizer.

The following are demos of each individual function:

1. Parse: Type Ctrl/Cmd + Shift + P with your cursor in a .lts file and enter "LTS+: Build.Parse"

   

2. Compile: Type Ctrl/Cmd + Shift + P with your cursor in a .lts file and enter "LTS+: Build.Compile"

   

3. Compose: Type Ctrl/Cmd + Shift + P with your cursor in a .lts file, enter "LTS+: Build.Compose" and when prompted, choose a process to compose

   

4. Check Safety: Type Ctrl/Cmd + Shift + P with your cursor in a .lts file and enter "LTS+: Check.Safety" and when prompted, choose a process to compose

   

5. Check Progress: Type Ctrl/Cmd + Shift + P with your cursor in a .lts file and enter "LTS+: Check.Progress" and when prompted, choose a process to compose

   

6. Check Property: Type Ctrl/Cmd + Shift + P with your cursor in a .lts file and enter "LTS+: Check.Property", when prompted, choose a process to compose and a property to assert