### Example FT Semantics for PackageInstallation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/after_null_null_satisfaction.md

This is a specific example of the '[after,null,null,satisfaction]' pattern, illustrating how the system should satisfy a post-condition after a package installation.

```plaintext
((!`last_in_PackageInstallation`) U (`last_in_PackageInstallation` & (X (F ( `indicationLight` = `orange` ))))) | (G (!`last_in_PackageInstallation`))
```

--------------------------------

### Install FRET Dependencies and Start Application

Source: https://context7.com/nasa-sw-vnv/fret/llms.txt

Navigate to the fret-electron directory and run npm scripts to install dependencies, start FRET in production mode, or start in development mode with hot reloading.

```bash
cd fret/fret-electron
npm run fret-install
npm run start
npm run dev
```

--------------------------------

### Example FT Semantics: Package Installation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/before_null_always_satisfaction.md

This example demonstrates the FT semantics for a specific scenario: before PackageInstallation, the system must always satisfy the condition 'indicationLight = orange'. This is enforced strictly before the first occurrence of PackageInstallation.

```fret
(F `first_in_PackageInstallation`) -> (!((!`first_in_PackageInstallation`) U ((!( `indicationLight` = `orange` )) & (!`first_in_PackageInstallation`))))
```

--------------------------------

### Install WSL and Ubuntu

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/installingFRET/installation_windows.md

Run this command in Windows Powershell or Command Prompt to install WSL and a default Ubuntu distribution. This is the recommended starting point for FRET installation on Windows.

```bash
wsl --install
```

--------------------------------

### Example FT Semantics for Package Installation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/in_regular_always_action.md

Illustrates the Forwarding Trace (FT) semantics for a specific scenario: in PackageInstallation, when lowLevel is greater than highLevel, the system shall always reset System.

```plaintext
G (((`lowLevel` > `highLevel`) & `PackageInstallation`) -> `reset` `System`)
```

--------------------------------

### Example: after PackageInstallation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/after_null_after_action.md

An example illustrating the [after,null,after,action] pattern where a system reset is enforced after PackageInstallation. It specifies a time duration for the action.

```FT Semantics
((!`last_in_PackageInstallation`) U (`last_in_PackageInstallation` & (X (((!`reset` `System`) & (!(F[10 `secs`] (!(!`reset` `System`))))) & (`reset` `System` | (F[10 `secs`+1] `reset` `System`)))))) | (G (!`last_in_PackageInstallation`))
```

--------------------------------

### Example FT Semantics for [after,null,within,action] Pattern

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/after_null_within_action.md

An example demonstrating the FT Semantics for the [after,null,within,action] pattern, specifically for resetting a system after package installation within a time limit.

```fret
((!`last_in_PackageInstallation`) U (`last_in_PackageInstallation` & (X (`reset` `System` | (F[10 `secs`] `reset` `System`))))) | (G (!`last_in_PackageInstallation`))
```

--------------------------------

### Example PT Semantics for Package Installation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/in_regular_always_action.md

Illustrates the Production Trace (PT) semantics for a specific scenario: in PackageInstallation, when lowLevel is greater than highLevel, the system shall always reset System.

```plaintext
H (((`lowLevel` > `highLevel`) & `PackageInstallation`) -> `reset` `System`)
```

--------------------------------

### Install ltlsim-core with npm

Source: https://github.com/nasa-sw-vnv/fret/blob/master/tools/LTLSIM/ltlsim-core/Readme.md

Standard installation command for ltlsim-core using npm.

```bash
npm install
```

--------------------------------

### Fret Pattern Example: Package Installation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/in_regular_never_satisfaction.md

Example illustrating the Fret pattern in PackageInstallation context. It specifies that the indicationLight shall never be orange when lowLevel is greater than highLevel.

```text
G (((`lowLevel` > `highLevel`) & `PackageInstallation`) -> (!( `indicationLight` = `orange` )))
```

--------------------------------

### Install and Run LTLSIM

Source: https://github.com/nasa-sw-vnv/fret/blob/master/tools/LTLSIM/ltlsim-electron/README.md

Instructions for installing dependencies and running the LTLSIM tool using environment variables for formula and trace files.

```bash
cd tools/LTLSIM/ltlsim-core
npm install
cd ../ltlsim-electron
npm install

    export LTL_FORMULAFILE="formula.txt"; export LTL_TRACEFILE="trace.txt"; npm run dev
```

--------------------------------

### Example FT Semantics for PackageInstallation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/after_null_immediately_satisfaction.md

An example illustrating the FT semantics for the [after,null,immediately,satisfaction] pattern, specifically for the 'PackageInstallation' event and an 'indicationLight = orange' post-condition.

```fret
((!`last_in_PackageInstallation`) U (`last_in_PackageInstallation` & (X ( `indicationLight` = `orange` )))) | (G (!`last_in_PackageInstallation`))
```

--------------------------------

### Fret Pattern Example: Package Installation (PT Semantics)

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/in_regular_never_satisfaction.md

Example illustrating the Fret pattern in PackageInstallation context using PT Semantics. It specifies that the indicationLight shall never be orange when lowLevel is greater than highLevel.

```text
H (((`lowLevel` > `highLevel`) & `PackageInstallation`) -> (!( `indicationLight` = `orange` )))
```

--------------------------------

### Build and Start Fret Electron Application

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/developersGuide/installingAndRunningFRET.md

Combine the build and start steps into a single command using 'npm run bstart'. This is useful after making source code modifications.

```bash
npm run bstart
```

--------------------------------

### Install Node.js using nvm

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/installingFRET/installationInstructions.md

Install Node Version Manager (nvm) and then install Node.js version 20. Ensure your shell is reloaded after installing nvm.

```bash
# Download and install nvm:
curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.40.2/install.sh | bash

# in lieu of restarting the shell
. "$HOME/.nvm/nvm.sh"

# Download and install Node.js:
nvm install 20

# Verify the Node.js version:
node -v # Should print "v20.19.0".
nvm current # Should print "v20.19.0".

# Verify npm version:
npm -v # Should print "10.8.2".
```

--------------------------------

### Install Git on Ubuntu

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/installingFRET/installation_windows.md

If 'git' is not available in your Ubuntu WSL environment, install it using the apt package manager. This is necessary for cloning the FRET repository.

```bash
sudo apt install git
```

--------------------------------

### Clone FRET Repository and Install

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/installingFRET/installation_windows.md

Clone the FRET repository and navigate into the electron app directory. Then, run the installation script. Ensure you are within the Ubuntu WSL environment.

```bash
git clone https://github.com/NASA-SW-VnV/fret.git
cd fret/fret-electron
npm run fret-install
```

--------------------------------

### Example FT Semantics: System Satisfies Orange Light

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/null_null_within_satisfaction.md

Example FT Semantics illustrating a system satisfying the condition 'indicationLight = orange' within 10 seconds.

```text
( `indicationLight` = `orange` ) | (F[10 `secs`] ( `indicationLight` = `orange` ))
```

--------------------------------

### Example: Never Reset System Before PackageInstallation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/before_null_never_action.md

Illustrates the [before,null,never,action] pattern with a concrete example. The system shall never reset itself before the 'PackageInstallation' scope mode is first encountered.

```text
(F `first_in_PackageInstallation`) -> (!((!`first_in_PackageInstallation`) U ((!(!`reset` `System`)) & (!`first_in_PackageInstallation`))))
```

--------------------------------

### Example: FT Semantics in PackageInstallation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/in_regular_never_action.md

Illustrates the [in,regular,never,action] pattern with specific conditions in PackageInstallation. The system shall never reset System when lowLevel exceeds highLevel.

```text
G (((`lowLevel` > `highLevel`) & `PackageInstallation`) -> (!`reset` `System`))
```

--------------------------------

### Example: PT Semantics in PackageInstallation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/in_regular_never_action.md

Illustrates the [in,regular,never,action] pattern with specific conditions in PackageInstallation using PT Semantics. The system shall never reset System when lowLevel exceeds highLevel.

```text
H (((`lowLevel` > `highLevel`) & `PackageInstallation`) -> (!`reset` `System`))
```

--------------------------------

### Example FT Semantics for PackageInstallation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/after_null_after_satisfaction.md

Specific FT Semantics for the example scenario where the system must satisfy 'indicationLight = orange' after 'PackageInstallation'. This illustrates the application of the [after,null,after,satisfaction] pattern with concrete values for duration and conditions.

```fret
((!`last_in_PackageInstallation`) U (`last_in_PackageInstallation` & (X (((!( `indicationLight` = `orange` )) & (!(F[10 `secs`] (!(!( `indicationLight` = `orange` )))))) & (( `indicationLight` = `orange` ) | (F[10 `secs`+1] ( `indicationLight` = `orange` ))))))) | (G (!`last_in_PackageInstallation`))
```

--------------------------------

### Install electron-packager

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/installingFRET/buildingExecutables.md

Installs the electron-packager globally. This is a required dependency for building the FRET executable natively.

```bash
npm install -g electron-packager
```

--------------------------------

### Install FRET Dependencies

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/installingFRET/installationInstructions.md

Install FRET dependencies using npm. This command should be run from the fret-electron directory.

```bash
npm run fret-install
```

--------------------------------

### Example FT Semantics for PackageInstallation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/after_null_within_satisfaction.md

This snippet provides a concrete example of the FT Semantics for the [after,null,within,satisfaction] pattern, specifically for the PackageInstallation scenario. It illustrates the application of scope mode, duration, and post-condition.

```plaintext
((!`last_in_PackageInstallation`) U (`last_in_PackageInstallation` & (X (( `indicationLight` = `orange` ) | (F[10 `secs`] ( `indicationLight` = `orange` )))))) | (G (!`last_in_PackageInstallation`))
```

--------------------------------

### NuSMV Formula Example

Source: https://github.com/nasa-sw-vnv/fret/blob/master/tools/LTLSIM/ltlsim-electron/README.md

Example of a formula in NuSMV syntax. This format is used for defining properties to be verified.

```nusmv
H ((!((!RES) S ((!RES) & ((MODE & ((! Y TRUE) | (Y ! MODE))) & ((Y (H ! MODE)) | (! Y TRUE)))))) -> (O[0, 0] ((MODE & ((! Y TRUE) | (Y ! MODE))) & ((Y (H ! MODE)) | (! Y TRUE)))))
```

--------------------------------

### Validate ltlsim executable and NuSMV installation

Source: https://github.com/nasa-sw-vnv/fret/blob/master/tools/LTLSIM/ltlsim-core/Readme.md

Command to test the ltlsim executable and NuSMV installation. Expected output indicates both are operational.

```bash
ltlsim -c
```

--------------------------------

### Example Realizability Check with Diagnosis

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/cli/cli.md

Demonstrates running the 'realizability' command with specific options (jkind solver, diagnose, timeout) and displays the output, including connected components and diagnosis results.

```bash
fret/fret-electron$ npm run --silent start-cli -- realizability --solver jkind --diagnose --timeout 200 Liquid_mixer liquid_mixer
Checking realizability for Liquid_mixer:liquid_mixer...

Specification is unrealizable.
Diagnosing unrealizable connected component: cc2 ...
Result: UNREALIZABLE
Number of connected components (cc): 6
┌─────────┬────────────────┬──────────┐
│ (index) │     Result     │   Time   │
├─────────┼────────────────┼──────────┤
│   cc0   │  'REALIZABLE'  │ '0.659s' │
│   cc1   │  'REALIZABLE'  │ '0.81s'  │
│   cc2   │ 'UNREALIZABLE' │ '0.609s' │
│   cc3   │  'REALIZABLE'  │ '0.998s' │
│   cc4   │  'REALIZABLE'  │ '0.904s' │
│   cc5   │  'REALIZABLE'  │ '1.058s' │
└─────────┴────────────────┴──────────┘

Diagnosis results for connected component cc2:
┌────────────┬──────────────────────┐
│  (index)   │     Requirements     │
├────────────┼──────────────────────┤
│ Conflict 1 │ [ 'LM001', 'LM009' ] │
└────────────┴──────────────────────┘
```

--------------------------------

### Example LTL Simulation Output

Source: https://github.com/nasa-sw-vnv/fret/blob/master/tools/LTLSIM/ltlsim-core/Readme.md

Example output from testing the Javascript wrapper, demonstrating LTL formula evaluations and simulation exit codes.

```text
[LTLSIM] Up and running ...
[NUSMV ] Up and running ...

```

```text
F1_1: ( G [0,4] hello )
F1_2: ( F [0,2] world )
F2 : 0,0,0,0,0,0,0,0,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0,0 => FALSE
ltlsim exited with code 0.
F1 : 0,0,0,0,1,1,1,1,1,1,1,1,1,1,0,0,0,0,0,1,1,1,1,1 => FALSE
F1 (F1_1) : 1,1,1,1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,0,0,0,0,0 => TRUE
F1 (F1_2) : 0,0,0,0,1,1,1,1,1,1,1,1,1,1,0,0,0,0,0,1,1,1,0,0 => FALSE
ltlsim exited with code 0.

```

--------------------------------

### Example of onlyAfter Pattern

Source: https://github.com/nasa-sw-vnv/fret/blob/master/fret-electron/docs/_media/semantics/patterns/onlyAfter_regular_after_satisfaction.md

Illustrates the intended meaning of the 'onlyAfter' pattern in Fret semantics. This example shows a conditional system satisfaction after a delay.

```fret
only after PackageInstallation,  when lowLevel > highLevel, shall the system  after 10 secs satisfy (indicationLight = orange)
```

--------------------------------

### LTLSim Simulation Output Example

Source: https://github.com/nasa-sw-vnv/fret/blob/master/tools/LTLSIM/ltlsim-core/Readme.md

This is an example of the output generated by the LTLSim simulation. It shows the evaluation results for formulas and subexpressions, along with exit codes.

```text
F2 : 0,0,0,0,0,0,0,0,0,1,1,1,1,1,0,0,0,0,0,0,0,0,0,0 => FALSE
ltlsim exited with code 0.
F1 : 0,0,0,0,1,1,1,1,1,1,1,1,1,1,0,0,0,0,0,1,1,1,1,1 => FALSE
F1 (F1_1) : 1,1,1,1,0,0,0,0,0,0,0,0,0,0,1,1,1,1,1,0,0,0,0,0 => TRUE
F1 (F1_2) : 0,0,0,0,1,1,1,1,1,1,1,1,1,1,0,0,0,0,0,1,1,1,0,0 => FALSE
ltlsim exited with code 0.
```