(EXPERIMENTAL) Explores the state space of an LF program. More...

Public Member Functions
void	addInitialEvents (ReactorInstance reactor)
	Recursively add the first events to the event queue.
void	explore (Tag horizon, boolean findLoop)
	Explore the state space and populate the state space diagram until the specified horizon (i.e.
	StateSpaceExplorer (ReactorInstance main)

Public Attributes
StateSpaceDiagram	diagram = new StateSpaceDiagram()
EventQueue	eventQ = new EventQueue()
	Instantiate a global event queue.
boolean	loopFound = false
ReactorInstance	main
	The main reactor instance based on which the state space is explored.

Detailed Description

(EXPERIMENTAL) Explores the state space of an LF program.

Use with caution since this is experimental code.

Constructor & Destructor Documentation

◆ StateSpaceExplorer()

org.lflang.analyses.statespace.StateSpaceExplorer.StateSpaceExplorer ( ReactorInstance main )

Member Function Documentation

◆ addInitialEvents()

void org.lflang.analyses.statespace.StateSpaceExplorer.addInitialEvents ( ReactorInstance reactor )

Recursively add the first events to the event queue.

◆ explore()

void org.lflang.analyses.statespace.StateSpaceExplorer.explore	(	Tag	horizon,
		boolean	findLoop )

Explore the state space and populate the state space diagram until the specified horizon (i.e.

the end tag) is reached OR until the event queue is empty.

As an optimization, if findLoop is true, the algorithm tries to find a loop in the state space during exploration. If a loop is found (i.e. a previously encountered state is reached again) during exploration, the function returns early.

TODOs: 1. Handle action with 0 minimum delay.

Note: This is experimental code which is to be refactored in a future PR. Use with caution.

Member Data Documentation

◆ diagram

StateSpaceDiagram org.lflang.analyses.statespace.StateSpaceExplorer.diagram = new StateSpaceDiagram()

◆ eventQ

EventQueue org.lflang.analyses.statespace.StateSpaceExplorer.eventQ = new EventQueue()

Instantiate a global event queue.

We will use this event queue to symbolically simulate the logical timeline. This simulation is also valid for runtime implementations that are federated or relax global barrier synchronization, since an LF program defines a unique logical timeline (assuming all reactions behave consistently throughout the execution).

◆ loopFound

boolean org.lflang.analyses.statespace.StateSpaceExplorer.loopFound = false

◆ main

ReactorInstance org.lflang.analyses.statespace.StateSpaceExplorer.main

The main reactor instance based on which the state space is explored.

The documentation for this class was generated from the following file:

/Users/runner/work/lingua-franca/lingua-franca/core/src/main/java/org/lflang/analyses/statespace/StateSpaceExplorer.java

Public Member Functions

Public Attributes