org.lflang.analyses.uclid.UclidGenerator Class Reference

(EXPERIMENTAL) Generator for Uclid5 models. More...

Inherits org.lflang.generator.GeneratorBase.

Classes
enum	Tactic
	A tactic used to verify properties. More...

Public Member Functions
void	doGenerate (Resource resource, LFGeneratorContext context)
	Generate code from the Lingua Franca model contained by the specified resource.
boolean	errorsOccurred ()
	Return true if errors occurred in the last call to doGenerate().
GeneratorCommandFactory	getCommandFactory ()
Instantiation	getMainDef ()
int	getReactionBankIndex (Reaction reaction)
	Return the reaction bank index.
Target	getTarget ()
	Return the Targets enum for the current target.
TargetConfig	getTargetConfig ()
TargetTypes	getTargetTypes ()
void	printInfo (LFGeneratorContext context)
	Print to stdout information about what source file is being generated, what mode the generator is in, and where the generated sources are to be put.
void	reportCommandErrors (String stderr)
	Parse the specified string for command errors that can be reported using marks in the Eclipse IDE.
void	setReactionBankIndex (Reaction reaction, int bankIndex)
	Mark the specified reaction to belong to only the specified bank index.
	UclidGenerator (LFGeneratorContext context, List< Attribute > properties)
	Constructor.

Public Attributes
List< ActionInstance >	actionInstances = new ArrayList<ActionInstance>()
	A list of action instances.
final LFGeneratorContext	context
int	CT = 0
	Completeness threshold.
Map< Path, String >	expectations = new HashMap<>()
List< Path >	generatedFiles = new ArrayList<>()
	A list of paths to the uclid files generated.
boolean	hasModalReactors = false
	Indicates whether the current Lingua Franca program contains model reactors.
boolean	hasWatchdogs = false
	Indicates whether the program has any watchdogs.
ReactorInstance	main
	The main (top-level) reactor instance.
MessageReporter	messageReporter
	An error reporter for reporting any errors or warnings during the code generation.
List< NamedInstance >	namedInstances
Path	outputDir
	The directory where the generated files are placed.
List< ReactionInstance.Runtime >	reactionInstances
	A list of reaction runtime instances.
UclidRunner	runner
	A runner for the generated Uclid files.
List< TriggerInstance >	triggerInstances
	Joint lists of the lists above.

Protected Member Functions
void	additionalPostProcessingForModes ()
	Hook for additional post-processing of the model.
boolean	buildUsingDocker ()
	Create Dockerfiles and docker-compose.yml, build, and create a launcher.
void	checkModalReactorSupport (boolean isSupported)
	Checks whether modal reactors are present and require appropriate code generation.
void	checkWatchdogSupport (boolean isSupported)
	Check whether watchdogs are present and are supported.
void	cleanIfNeeded (LFGeneratorContext context)
	Check if a clean was requested from the standalone compiler and perform the clean step.
void	copyUserFiles (TargetConfig targetConfig, FileConfig fileConfig)
	Copy user specific files to the src-gen folder.
void	createMainInstantiation ()
	If there is a main or federated reactor, then create a synthetic Instantiation for that top-level reactor and set the field mainDef to refer to it.
void	generateActionAxioms ()
	Generate axiomatic semantics for actions.
void	generateConnectionAxioms ()
	Generate axiomatic semantics for connections.
void	generateControlBlock ()
	Uclid5 control block.
void	generateInitialConditions ()
	Macros for initial conditions.
void	generateProperty ()
void	generateReactionAxioms ()
	Lift reaction bodies into Uclid axioms.
void	generateReactionIdsAndStateVars ()
	Type definitions for runtime reaction Ids and state variables.
void	generateReactionTriggerAxioms ()
	Axioms for encoding how reactions are triggered.
void	generateReactorSemantics ()
	Axioms for reactor semantics.
void	generateTimerAxioms ()
	Generate axiomatic semantics for timers.
void	generateTimingSemantics ()
	Macros for timing semantics.
void	generateTraceDefinition ()
	Macros, type definitions, and variable declarations for trace (path).
void	generateTriggersAndReactions ()
	Axioms for all triggers.
void	generateUclidCode ()
	The main function that generates Uclid code.
void	generateUclidFile ()
	Generate the Uclid model.
String	getConflictingConnectionsInModalReactorsBody (VarRef source, VarRef dest)
	Return target code for forwarding reactions iff the connections have the same destination as other connections or reaction in mutually exclusive modes.
DockerGenerator	getDockerGenerator (LFGeneratorContext context)
	Return a DockerGenerator instance suitable for the target.
ErrorFileAndLine	parseCommandOutput (String line)
	Given a line of text from the output of a compiler, return an instance of ErrorFileAndLine if the line is recognized as the first line of an error message.
void	registerTransformation (AstTransformation transformation)
	Register an AST transformation to be applied to the AST.
void	setReactorsAndInstantiationGraph (LFGeneratorContext.Mode mode)
	Create a new instantiation graph.

Protected Attributes
GeneratorCommandFactory	commandFactory
	A factory for compiler commands.
InstantiationGraph	instantiationGraph
	Graph that tracks dependencies between instantiations.
Instantiation	mainDef
	Definition of the main (top-level) reactor.
Map< Reaction, Integer >	reactionBankIndices = null
	Map from reactions to bank indices.
List< Reactor >	reactors = new ArrayList<>()
	A list of Reactor definitions in the main resource, including non-main reactors defined in imported resources.
final TargetConfig	targetConfig
	The current target configuration.

Detailed Description

(EXPERIMENTAL) Generator for Uclid5 models.

Constructor & Destructor Documentation

UclidGenerator()

org.lflang.analyses.uclid.UclidGenerator.UclidGenerator	(	LFGeneratorContext	context,
		List< Attribute >	properties )

Constructor.

Member Function Documentation

additionalPostProcessingForModes()

void org.lflang.generator.GeneratorBase.additionalPostProcessingForModes ( )

protectedinherited

Hook for additional post-processing of the model.

buildUsingDocker()

boolean org.lflang.generator.GeneratorBase.buildUsingDocker ( )

protectedinherited

Create Dockerfiles and docker-compose.yml, build, and create a launcher.

checkModalReactorSupport()

void org.lflang.generator.GeneratorBase.checkModalReactorSupport ( boolean isSupported )

protectedinherited

Checks whether modal reactors are present and require appropriate code generation.

This will set the hasModalReactors variable.

Parameters

isSupported

indicates if modes are supported by this code generation.

checkWatchdogSupport()

void org.lflang.generator.GeneratorBase.checkWatchdogSupport ( boolean isSupported )

protectedinherited

Check whether watchdogs are present and are supported.

Parameters

isSupported

indicates whether or not this is a supported target and whether or not it is a threaded runtime.

cleanIfNeeded()

void org.lflang.generator.GeneratorBase.cleanIfNeeded ( LFGeneratorContext context )

protectedinherited

Check if a clean was requested from the standalone compiler and perform the clean step.

copyUserFiles()

void org.lflang.generator.GeneratorBase.copyUserFiles ( TargetConfig targetConfig, FileConfig fileConfig )

protectedinherited

Copy user specific files to the src-gen folder.

This should be overridden by the target generators.

Parameters

targetConfig	The targetConfig to read the files from.
fileConfig	The fileConfig used to make the copy and resolve paths.

createMainInstantiation()

void org.lflang.generator.GeneratorBase.createMainInstantiation ( )

protectedinherited

If there is a main or federated reactor, then create a synthetic Instantiation for that top-level reactor and set the field mainDef to refer to it.

doGenerate()

void org.lflang.analyses.uclid.UclidGenerator.doGenerate	(	Resource	resource,
		LFGeneratorContext	context )

Generate code from the Lingua Franca model contained by the specified resource.

This is the main entry point for code generation. This base class finds all reactor class definitions, including any reactors defined in imported .lf files (except any main reactors in those imported files), and adds them to the reactors list. If errors occur during generation, then a subsequent call to errorsOccurred() will return true.

Parameters

resource	The resource containing the source code.
context	Context relating to invocation of the code generator. In standalone mode, this object is also used to relay CLI arguments.

Reimplemented from org.lflang.generator.GeneratorBase.

errorsOccurred()

boolean org.lflang.generator.GeneratorBase.errorsOccurred ( )

inherited

Return true if errors occurred in the last call to doGenerate().

This will return true if any of the reportError methods was called.

Returns

True if errors occurred.

generateActionAxioms()

void org.lflang.analyses.uclid.UclidGenerator.generateActionAxioms ( )

protected

Generate axiomatic semantics for actions.

generateConnectionAxioms()

void org.lflang.analyses.uclid.UclidGenerator.generateConnectionAxioms ( )

protected

Generate axiomatic semantics for connections.

generateControlBlock()

void org.lflang.analyses.uclid.UclidGenerator.generateControlBlock ( )

protected

Uclid5 control block.

generateInitialConditions()

void org.lflang.analyses.uclid.UclidGenerator.generateInitialConditions ( )

protected

Macros for initial conditions.

generateProperty()

void org.lflang.analyses.uclid.UclidGenerator.generateProperty ( )

protected

generateReactionAxioms()

void org.lflang.analyses.uclid.UclidGenerator.generateReactionAxioms ( )

protected

Lift reaction bodies into Uclid axioms.

generateReactionIdsAndStateVars()

void org.lflang.analyses.uclid.UclidGenerator.generateReactionIdsAndStateVars ( )

protected

Type definitions for runtime reaction Ids and state variables.

generateReactionTriggerAxioms()

void org.lflang.analyses.uclid.UclidGenerator.generateReactionTriggerAxioms ( )

protected

Axioms for encoding how reactions are triggered.

generateReactorSemantics()

void org.lflang.analyses.uclid.UclidGenerator.generateReactorSemantics ( )

protected

Axioms for reactor semantics.

generateTimerAxioms()

void org.lflang.analyses.uclid.UclidGenerator.generateTimerAxioms ( )

protected

Generate axiomatic semantics for timers.

generateTimingSemantics()

void org.lflang.analyses.uclid.UclidGenerator.generateTimingSemantics ( )

protected

Macros for timing semantics.

generateTraceDefinition()

void org.lflang.analyses.uclid.UclidGenerator.generateTraceDefinition ( )

protected

Macros, type definitions, and variable declarations for trace (path).

generateTriggersAndReactions()

void org.lflang.analyses.uclid.UclidGenerator.generateTriggersAndReactions ( )

protected

Axioms for all triggers.

generateUclidCode()

void org.lflang.analyses.uclid.UclidGenerator.generateUclidCode ( )

protected

The main function that generates Uclid code.

generateUclidFile()

void org.lflang.analyses.uclid.UclidGenerator.generateUclidFile ( )

protected

Generate the Uclid model.

getCommandFactory()

GeneratorCommandFactory org.lflang.generator.GeneratorBase.getCommandFactory ( )

inherited

getConflictingConnectionsInModalReactorsBody()

String org.lflang.generator.GeneratorBase.getConflictingConnectionsInModalReactorsBody ( VarRef source, VarRef dest )

protectedinherited

Return target code for forwarding reactions iff the connections have the same destination as other connections or reaction in mutually exclusive modes.

This method needs to be overridden in target specific code generators that support modal reactors.

getDockerGenerator()

DockerGenerator org.lflang.analyses.uclid.UclidGenerator.getDockerGenerator ( LFGeneratorContext context )

protected

Return a DockerGenerator instance suitable for the target.

Reimplemented from org.lflang.generator.GeneratorBase.

getMainDef()

Instantiation org.lflang.generator.GeneratorBase.getMainDef ( )

inherited

getReactionBankIndex()

int org.lflang.generator.GeneratorBase.getReactionBankIndex ( Reaction reaction )

inherited

Return the reaction bank index.

See also

setReactionBankIndex

Parameters

reaction

The reaction.

Returns

The reaction bank index, if one has been set, and -1 otherwise.

getTarget()

Target org.lflang.analyses.uclid.UclidGenerator.getTarget

(

)

Return the Targets enum for the current target.

Reimplemented from org.lflang.generator.GeneratorBase.

getTargetConfig()

TargetConfig org.lflang.generator.GeneratorBase.getTargetConfig ( )

inherited

getTargetTypes()

TargetTypes org.lflang.analyses.uclid.UclidGenerator.getTargetTypes

(

)

Reimplemented from org.lflang.generator.GeneratorBase.

parseCommandOutput()

ErrorFileAndLine org.lflang.generator.GeneratorBase.parseCommandOutput ( String line )

protectedinherited

Given a line of text from the output of a compiler, return an instance of ErrorFileAndLine if the line is recognized as the first line of an error message.

Otherwise, return null. This base class simply returns null.

Parameters

line	A line of output from a compiler or other external tool that might generate errors.

Returns

If the line is recognized as the start of an error message, then return a class containing the path to the file on which the error occurred (or null if there is none), the line number (or the string "1" if there is none), the character position (or the string "0" if there is none), and the message (or an empty string if there is none).

printInfo()

void org.lflang.generator.GeneratorBase.printInfo ( LFGeneratorContext context )

inherited

Print to stdout information about what source file is being generated, what mode the generator is in, and where the generated sources are to be put.

registerTransformation()

void org.lflang.generator.GeneratorBase.registerTransformation ( AstTransformation transformation )

protectedinherited

Register an AST transformation to be applied to the AST.

The transformations will be applied in the order that they are registered in.

reportCommandErrors()

void org.lflang.generator.GeneratorBase.reportCommandErrors ( String stderr )

inherited

Parse the specified string for command errors that can be reported using marks in the Eclipse IDE.

In this class, we attempt to parse the messages to look for file and line information, thereby generating marks on the appropriate lines. This should not be called in standalone mode.

Parameters

stderr

The output on standard error of executing a command.

setReactionBankIndex()

void org.lflang.generator.GeneratorBase.setReactionBankIndex ( Reaction reaction, int bankIndex )

inherited

Mark the specified reaction to belong to only the specified bank index.

This is needed because reactions cannot declare a specific bank index as an effect or trigger. Reactions that send messages between federates, including absent messages, need to be specific to a bank member.

Parameters

reaction	The reaction.
bankIndex	The bank index, or -1 if there is no bank.

setReactorsAndInstantiationGraph()

void org.lflang.generator.GeneratorBase.setReactorsAndInstantiationGraph ( LFGeneratorContext.Mode mode )

protectedinherited

Create a new instantiation graph.

This is a graph where each node is a Reactor (not a ReactorInstance) and an arc from Reactor A to Reactor B means that B contains an instance of A, constructed with a statement like a = new A(); After creating the graph, sort the reactors in topological order and assign them to the reactors class variable. Hence, after this method returns, this.reactors will be a list of Reactors such that any reactor is preceded in the list by reactors that it instantiates.

Member Data Documentation

actionInstances

List<ActionInstance> org.lflang.analyses.uclid.UclidGenerator.actionInstances = new ArrayList<ActionInstance>()

A list of action instances.

commandFactory

GeneratorCommandFactory org.lflang.generator.GeneratorBase.commandFactory

protectedinherited

A factory for compiler commands.

context

final LFGeneratorContext org.lflang.generator.GeneratorBase.context

inherited

CT

int org.lflang.analyses.uclid.UclidGenerator.CT = 0

Completeness threshold.

expectations

Map<Path, String> org.lflang.analyses.uclid.UclidGenerator.expectations = new HashMap<>()

generatedFiles

List<Path> org.lflang.analyses.uclid.UclidGenerator.generatedFiles = new ArrayList<>()

A list of paths to the uclid files generated.

hasModalReactors

boolean org.lflang.generator.GeneratorBase.hasModalReactors = false

inherited

Indicates whether the current Lingua Franca program contains model reactors.

hasWatchdogs

boolean org.lflang.generator.GeneratorBase.hasWatchdogs = false

inherited

Indicates whether the program has any watchdogs.

This is used to check for support.

instantiationGraph

InstantiationGraph org.lflang.generator.GeneratorBase.instantiationGraph

protectedinherited

Graph that tracks dependencies between instantiations.

This is a graph where each node is a Reactor (not a ReactorInstance) and an arc from Reactor A to Reactor B means that B contains an instance of A, constructed with a statement like a = new A(); After creating the graph, sort the reactors in topological order and assign them to the reactors class variable. Hence, after this method returns, this.reactors will be a list of Reactors such that any reactor is preceded in the list by reactors that it instantiates.

main

ReactorInstance org.lflang.generator.GeneratorBase.main

inherited

The main (top-level) reactor instance.

mainDef

Instantiation org.lflang.generator.GeneratorBase.mainDef

protectedinherited

Definition of the main (top-level) reactor.

This is an automatically generated AST node for the top-level reactor.

messageReporter

MessageReporter org.lflang.generator.GeneratorBase.messageReporter

inherited

An error reporter for reporting any errors or warnings during the code generation.

namedInstances

List<NamedInstance> org.lflang.analyses.uclid.UclidGenerator.namedInstances

outputDir

Path org.lflang.analyses.uclid.UclidGenerator.outputDir

The directory where the generated files are placed.

reactionBankIndices

Map<Reaction, Integer> org.lflang.generator.GeneratorBase.reactionBankIndices = null

protectedinherited

Map from reactions to bank indices.

reactionInstances

List<ReactionInstance.Runtime> org.lflang.analyses.uclid.UclidGenerator.reactionInstances

Initial value:

=
      new ArrayList<ReactionInstance.Runtime>()

A list of reaction runtime instances.

reactors

List<Reactor> org.lflang.generator.GeneratorBase.reactors = new ArrayList<>()

protectedinherited

A list of Reactor definitions in the main resource, including non-main reactors defined in imported resources.

These are ordered in the list in such a way that each reactor is preceded by any reactor that it instantiates using a command like foo = new Foo();

runner

UclidRunner org.lflang.analyses.uclid.UclidGenerator.runner

A runner for the generated Uclid files.

targetConfig

final TargetConfig org.lflang.generator.GeneratorBase.targetConfig

protectedinherited

The current target configuration.

triggerInstances

List<TriggerInstance> org.lflang.analyses.uclid.UclidGenerator.triggerInstances

Joint lists of the lists above.

---

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/uclid/UclidGenerator.java