org.lflang.analyses.uclid.UclidRunner Class Reference

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

Public Member Functions
StateInfo	parseStateInfo (String smtStr)
	Parse information from an SMT model for a step in the trace.
void	run ()
	Run all the generated Uclid models, report outputs, and generate counterexample trace diagrams.
	UclidRunner (UclidGenerator generator)

Package Attributes
GeneratorCommandFactory	commandFactory
	A factory for compiler commands.
UclidGenerator	generator
	A UclidGenerator instance.
MessageReporter	reporter

Detailed Description

(EXPERIMENTAL) Runner for Uclid5 models.

Constructor & Destructor Documentation

UclidRunner()

org.lflang.analyses.uclid.UclidRunner.UclidRunner

(

UclidGenerator

generator

)

Member Function Documentation

parseStateInfo()

StateInfo org.lflang.analyses.uclid.UclidRunner.parseStateInfo

(

String

smtStr

)

Parse information from an SMT model for a step in the trace.

run()

void org.lflang.analyses.uclid.UclidRunner.run

(

)

Run all the generated Uclid models, report outputs, and generate counterexample trace diagrams.

Member Data Documentation

commandFactory

GeneratorCommandFactory org.lflang.analyses.uclid.UclidRunner.commandFactory

package

A factory for compiler commands.

generator

UclidGenerator org.lflang.analyses.uclid.UclidRunner.generator

package

A UclidGenerator instance.

reporter

MessageReporter org.lflang.analyses.uclid.UclidRunner.reporter

package

---

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/UclidRunner.java