envgen.codegen
Class LTLDriverGenerator

java.lang.Object
  |
  +--envgen.codegen.AbstractDriverGenerator
        |
        +--envgen.codegen.JavaDriverGenerator
              |
              +--envgen.codegen.LTLDriverGenerator

All Implemented Interfaces:

ICodeGenerator

public class LTLDriverGenerator

extends JavaDriverGenerator

Generates drivers based on user-supplied ltl assumptions.

Field Summary

(package private) int	debug Set to print debugging messages.
(package private) boolean	singleEventCond

Fields inherited from class envgen.codegen.JavaDriverGenerator

atomicStepsMode, defaultInstantiations, defaultPropositions

Fields inherited from class envgen.codegen.AbstractDriverGenerator

envTable, unitInterface, unitTable, userSpec

Constructor Summary

LTLDriverGenerator(java.util.HashMap unitTable, java.util.HashMap envTable, UnitInterface unitInterface)

Method Summary

soot.Body	createSynthesizedRunBody(FSA fsa, java.util.List propositions)
void	genMainFromSpec(soot.util.Chain units)
protected soot.SootClass	genThread(FSA fsa, java.util.List propositions, java.lang.String threadName) Constructs a soot class that represents a thread synthesized from an LTL specification.
void	genThreads() Reads thread specifications one by one and synthesizes threads from them.

Methods inherited from class envgen.codegen.JavaDriverGenerator

genAssignmentStmt, genAtomicPropStmt, genMainRunBody, genMainThread, genMethodStmt, genPropositionStmt, genThreadBasics, genThreadConstructorBody, genTryCatchStmt

Methods inherited from class envgen.codegen.AbstractDriverGenerator

genCode

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

singleEventCond

boolean singleEventCond

debug

int debug

Set to print debugging messages.

Constructor Detail

LTLDriverGenerator

public LTLDriverGenerator(java.util.HashMap unitTable,
                          java.util.HashMap envTable,
                          UnitInterface unitInterface)

Method Detail

genThreads

public void genThreads()

Reads thread specifications one by one and synthesizes threads from them.

Specified by:

genThreads in class AbstractDriverGenerator

genMainFromSpec

public void genMainFromSpec(soot.util.Chain units)

Specified by:

genMainFromSpec in class JavaDriverGenerator

genThread

protected soot.SootClass genThread(FSA fsa,
                                   java.util.List propositions,
                                   java.lang.String threadName)

Constructs a soot class that represents a thread synthesized from an LTL specification.

createSynthesizedRunBody

public soot.Body createSynthesizedRunBody(FSA fsa,
                                          java.util.List propositions)