The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems.
PLEXIL Formal Interactive Verification Environment (PLEXIL-V) is a tool that contains a formal executable semantics of PLEXIL specified as a rewriting logic specification in the Maude system.
PLEXIL-V provides an LTL model-checker of PLEXIL plans and a framework to model PLEXIL execution environments for verification.
PLEXIL-V v0.6.4 (November 2026)
-
The Maude System: Binary releases for different platforms can be found here.
-
Python (>= 3.10): Binary releases for different platforms can be found here.
The components of PLEXIL-V are organized in the following directories:
plexil2maudetranslator from PLEXIL XML format to PLEXIL-V internal format.pythonintegrated command line interface (calledplexilv) for different PLEXIL-V tools and workflows, including log processing tools.plexilgit submodule with the official PLEXIL executive version that is supported by PLEXIL-V.semanticsthe rewriting logic specification in Maude that implements the formal semantics and the auxiliary tools needed for model-checking and modeling execution environments.examplesfor showcasing how to verify properties of PLEXIL plans.
From the root of the repository, create a Python virtual environment and load it to be able to install packages:
$ python3 -m venv .venv
$ source .venv/bin/activate
Then, install all the Python packages located in python (including plexilv-cli) in development mode with:
$ python/install_all.sh
The script force-reinstalls the packages ignoring pip caches, so it is also the command to run after pulling changes, since package versions are not bumped between them.
Immediately after, confirm that plexilv is accessible from the command line by running:
$ plexilv
$ plexilv run --help
$ plexilv diff --help
The virtual environment is only active in the terminal where you ran source .venv/bin/activate (your prompt shows (.venv) while it is active).
Whenever you open a new terminal, activate it again from the root of the repository before using plexilv or any of the other Python tools, such as plx2maude:
$ source .venv/bin/activate
To install the official PLEXIL executive, checkout the plexil submodule of this repository:
$ git submodule update --init --recursive
Then follow the instructions located in the official repository.
If you run into issues while compiling, the minimal set of tools needed for PLEXIL-V can be obtained by running the following commands from the plexil folder:
$ make ipc
$ make tools -j
After adding the plexil/scripts folder to the PATH environment variable, the following commands should be available:
$ plexilc
$ plexiltest
The semantics is inside the semantics/src/ folder.
The file that needs to be imported to access all the semantics is the semantics/src/plexil-v.maude file:
$ maude semantics/src/plexil-v.maude
The PLEXIL-V module should be visible.
Maude> show module PLEXIL-V .
The examples/ folder, contains some examples of PLEXIL plans with properties to verify.
The examples use the Python tools installed above, so make sure the virtual environment is active in your terminal (source .venv/bin/activate from the root of the repository).
As a verification example, let's use TakeImage0 folder, which contains a PLEXIL plan controlling a camera that can move to point at its target before taking a photo, if necessary.
Two environment model files are provided to model the environment of execution of the plan.
env0.maude models an environment in which the camera is always pointing at its target, while env1.maude models that the camera can be moved away from the target at any execution step.
The example properties to verify are contained in properties.maude.
Some Maude scripts are provided to automate the loading and execution of the models:
loadX.maudescripts load theTakeImage0plan and the environmentenvX.maude.check.maudecontains the commands to execute to verify the different properties. Before executing any of the previous scripts the PLEXIL-V main moduleplexil-v.maudehas to be loaded into Maude.
To verify the properties in env0.maude we would run the following commands:
$ cd examples/TakeImage0
$ make # compiles the plans
$ maude ../../semantics/src/plexil-v.maude load0.maude check.maude
Then we can confirm that all the properties hold:
...
==========================================
reduce in M-CHECK : plexilModelCheck(init, correctness1, transitionCounterexample) .
rewrites: 6872 in 1ms cpu (1ms real) (4032863 rewrites/second)
result Bool: true
==========================================
...
However, if we try to verify them over env-1.maude:
$ cd examples/TakeImage
$ maude ../../semantics/src/plexil-v.maude load1.maude check.maude
some of them fail:
...
==========================================
reduce in M-CHECK : plexilModelCheck(init, correctness1, transitionCounterexample) .
rewrites: 8316 in 2ms cpu (2ms real) (3977044 rewrites/second)
result TransitionCounterexample:
Start
-->
Input(stateLookup('PointedAtTarget, nilarg, val(true)))
-->
Input(commandAck('camera_capture_image, val(50) val(1), CommandSuccess) stateLookup('PointedAtTarget, nilarg, val(false)))
-->
Loop{
Input(stateLookup('PointedAtTarget, nilarg, val(true)))
--> Input(stateLookup('PointedAtTarget, nilarg, val(false)))
}
==========================================
...
Note that a counterexample is provided for each of the failures.
The example property correctness1, defined as hasStatus('TakeImage, executing) U hasStatus('TakeImage, finished), states that the root node of the plan remains in the EXECUTING status until it eventually reaches the FINISHED state.
This property clearly holds when the camera is always pointing at its target (as in env0.maude) but not if it can move (as in env1.maude), since in the latter case, an invariant condition in the plan is violated, preventing the root node from finishing.
Executing a plan in PLEXIL-V follows a similar approach to running tests with the plexiltest utility found in the official PLEXIL release.
First, you have an input .ple plan and input .pst script that you compile by using the official plexilc compiler into the internal PLEXIL XML formats .plx and .psx, respectively.
Then, you call the interpreter with the compiled files and observe the output.
For example, in the TakeImage0 example, the plan and script input files would be compiled like this:
$ cd examples/TakeImage0
$ plexilc TakeImage0.ple
$ plexilc script1.pst
And the PLEXIL-V formal interpreter would be invoked with the following command:
$ plexilv run -p TakeImage0.plx -s script1.psx
Currently, the output of the interpreter is the sequence of synchronous transitions performed by the plan.
PLEXIL-V now provides interactive stepper and debugger tools for step-by-step plan execution. These tools are in their initial version and offer two implementations:
PLEXIL-V Stepper - Based on the formal Maude semantics:
$ cd python/plexilv-stepper/plexilv-stepper
$ pip install -e .
$ plexilv-stepper -p plan.plx -s script.pst
PlexilTest Stepper/Debugger - Based on the PLEXIL TestExec:
$ cd python/plexilv-stepper/plexiltest-stepper-debugger
$ pip install .
$ plexiltest-stepper -p plan.plx -s script.pst
$ plexiltest-debugger -p plan.plx -s script.pst
The stepper allows you to execute plans one step at a time, inspect node states, and understand the execution flow. The debugger provides a graphical interface for visual plan exploration. Note that these tools are in active development and may have limited functionality compared to the batch verification tools.
See python/plexilv-stepper/README.md for detailed installation and usage instructions.
PLEXIL-V provides the plexilv diff utility to perform differential testing of the execution of a PLEXIL plan with multiple input scripts between the official PLEXIL test executor (plexiltest) and the PLEXIL-V formal interpreter (plexilv run).
First, you have an input .ple plan and multiple input .pst scripts that you compile into the internal PLEXIL XML formats .plx and .psx, respectively.
Then you call plexilv diff with all those inputs, obtaining a summary of differences found during execution.
For example, in the TakeImage0 example, the plan and scripts inputs would be compiled like this:
$ cd examples/TakeImage0
$ plexilc TakeImage0.ple
$ plexilc script0.pst
$ plexilc script1.pst
And the PLEXIL-V differential testing tool would be invoked like this:
$ plexilv diff -p TakeImage0.plx -s script0.psx -s script1.psx
The code in this repository is released under NASA's Open Source Agreement.
See the directory LICENSES; see also the copyright notice at the end of this file.
- Laura R. Humphrey (laura.r.humphrey@nasa.gov), NASA Langley Research Center, USA.
- Cesar A. Muñoz, NASA Langley Research Center, USA.
- Marco A. Feliu, Analytical Mechanics Associates supporting NASA Langley Research Center, USA.
- Camilo Rocha, Pontificia Universidad Javeriana de Cali, Colombia.
- Hector Cadavid, Escuela Colombiana de Ingeniería, Colombia.
Copyright 2016 United States Government as represented by the Administrator of the National Aeronautics and Space Administration. All Rights Reserved.
No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES IT "AS IS."
Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS AGREEMENT.