org.lflang.analyses.uclid.UclidGenerator.Tactic Enum Reference

A tactic used to verify properties. More...

Public Attributes
	BMC
	INDUCTION

Detailed Description

A tactic used to verify properties.

Currently, only BMC (bounded model checking) is functional. FIXME: For a future version that supports multiple tactics, the tactics should be stored in a list.

Member Data Documentation

BMC

org.lflang.analyses.uclid.UclidGenerator.Tactic.BMC

INDUCTION

org.lflang.analyses.uclid.UclidGenerator.Tactic.INDUCTION

---

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

• /Users/runner/work/lingua-franca/lingua-franca/core/src/main/java/org/lflang/analyses/uclid/UclidGenerator.java