(EXPERIMENTAL) Transpiler from an MTL specification to a Uclid axiom. More...

Inherits MTLParserBaseVisitor< String >.

Public Member Functions
String	_visitUnaryOp (MTLParser.UnaryOpContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
long	getHorizon ()
	Get the time horizon (in nanoseconds) of the property.
	MTLVisitor (Tactic tactic)
String	visitAtomicProp (MTLParser.AtomicPropContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitConjunction (MTLParser.ConjunctionContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitDifference (MTLParser.DifferenceContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitDisjunction (MTLParser.DisjunctionContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitEquivalence (MTLParser.EquivalenceContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitExpr (MTLParser.ExprContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitFinally (MTLParser.FinallyContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitGlobally (MTLParser.GloballyContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitImplication (MTLParser.ImplicationContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitMtl (MTLParser.MtlContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitNegation (MTLParser.NegationContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitNext (MTLParser.NextContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitNoUnaryOp (MTLParser.NoUnaryOpContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitPrimary (MTLParser.PrimaryContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitProduct (MTLParser.ProductContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitQuotient (MTLParser.QuotientContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitSum (MTLParser.SumContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)
String	visitUntil (MTLParser.UntilContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon)

Protected Attributes
CodeBuilder	code = new CodeBuilder()
	The main place to put generated code.
long	horizon = 0
	Time horizon (in nanoseconds) of the property.
Tactic	tactic
	Tactic to be used to prove the property.

Detailed Description

(EXPERIMENTAL) Transpiler from an MTL specification to a Uclid axiom.

Constructor & Destructor Documentation

◆ MTLVisitor()

org.lflang.analyses.uclid.MTLVisitor.MTLVisitor ( Tactic tactic )

Member Function Documentation

◆ _visitUnaryOp()

String org.lflang.analyses.uclid.MTLVisitor._visitUnaryOp	(	MTLParser.UnaryOpContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ getHorizon()

long org.lflang.analyses.uclid.MTLVisitor.getHorizon ( )

Get the time horizon (in nanoseconds) of the property.

◆ visitAtomicProp()

String org.lflang.analyses.uclid.MTLVisitor.visitAtomicProp	(	MTLParser.AtomicPropContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitConjunction()

String org.lflang.analyses.uclid.MTLVisitor.visitConjunction	(	MTLParser.ConjunctionContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitDifference()

String org.lflang.analyses.uclid.MTLVisitor.visitDifference	(	MTLParser.DifferenceContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitDisjunction()

String org.lflang.analyses.uclid.MTLVisitor.visitDisjunction	(	MTLParser.DisjunctionContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitEquivalence()

String org.lflang.analyses.uclid.MTLVisitor.visitEquivalence	(	MTLParser.EquivalenceContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitExpr()

String org.lflang.analyses.uclid.MTLVisitor.visitExpr	(	MTLParser.ExprContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitFinally()

String org.lflang.analyses.uclid.MTLVisitor.visitFinally	(	MTLParser.FinallyContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitGlobally()

String org.lflang.analyses.uclid.MTLVisitor.visitGlobally	(	MTLParser.GloballyContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitImplication()

String org.lflang.analyses.uclid.MTLVisitor.visitImplication	(	MTLParser.ImplicationContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitMtl()

String org.lflang.analyses.uclid.MTLVisitor.visitMtl	(	MTLParser.MtlContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitNegation()

String org.lflang.analyses.uclid.MTLVisitor.visitNegation	(	MTLParser.NegationContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitNext()

String org.lflang.analyses.uclid.MTLVisitor.visitNext	(	MTLParser.NextContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitNoUnaryOp()

String org.lflang.analyses.uclid.MTLVisitor.visitNoUnaryOp	(	MTLParser.NoUnaryOpContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitPrimary()

String org.lflang.analyses.uclid.MTLVisitor.visitPrimary	(	MTLParser.PrimaryContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitProduct()

String org.lflang.analyses.uclid.MTLVisitor.visitProduct	(	MTLParser.ProductContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitQuotient()

String org.lflang.analyses.uclid.MTLVisitor.visitQuotient	(	MTLParser.QuotientContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitSum()

String org.lflang.analyses.uclid.MTLVisitor.visitSum	(	MTLParser.SumContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

◆ visitUntil()

String org.lflang.analyses.uclid.MTLVisitor.visitUntil	(	MTLParser.UntilContext	ctx,
		String	prefixIdx,
		int	QFIdx,
		String	prevPrefixIdx,
		long	horizon )

Member Data Documentation

◆ code

CodeBuilder org.lflang.analyses.uclid.MTLVisitor.code = new CodeBuilder()

protected

The main place to put generated code.

◆ horizon

long org.lflang.analyses.uclid.MTLVisitor.horizon = 0

protected

Time horizon (in nanoseconds) of the property.

◆ tactic

Tactic org.lflang.analyses.uclid.MTLVisitor.tactic

protected

Tactic to be used to prove the property.

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

Public Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ MTLVisitor()

Member Function Documentation

◆ _visitUnaryOp()

◆ getHorizon()

◆ visitAtomicProp()

◆ visitConjunction()

◆ visitDifference()

◆ visitDisjunction()

◆ visitEquivalence()

◆ visitExpr()

◆ visitFinally()

◆ visitGlobally()

◆ visitImplication()

◆ visitMtl()

◆ visitNegation()

◆ visitNext()

◆ visitNoUnaryOp()

◆ visitPrimary()

◆ visitProduct()

◆ visitQuotient()

◆ visitSum()

◆ visitUntil()

Member Data Documentation

◆ code

◆ horizon

◆ tactic