ca.uqac.lif.ecp.ltl

Class GreedyLtlGenerator

java.lang.Object

ca.uqac.lif.ecp.TraceGenerator<T>

ca.uqac.lif.ecp.GreedyTraceGenerator<AtomicEvent>

ca.uqac.lif.ecp.ltl.GreedyLtlGenerator

public class GreedyLtlGenerator
extends GreedyTraceGenerator<AtomicEvent>

Greedy generator when the input specification is a finite-state automaton.

Author:

Sylvain Hallé

Field Summary

Fields

Modifier and Type	Field and Description
protected java.util.List<AtomicEvent>	m_alphabet The set of possible events.
protected Operator<AtomicEvent>	m_formula The LTL formula to generate against

Fields inherited from class ca.uqac.lif.ecp.GreedyTraceGenerator

m_lastCoverage, m_maxIterations, m_metric, m_numCandidates, m_random

Constructor Summary

Constructors

Constructor and Description
GreedyLtlGenerator(Operator<AtomicEvent> op, Alphabet<AtomicEvent> alph, java.util.Random random, CoverageMetric<AtomicEvent,java.lang.Float> metric)

Method Summary

Modifier and Type	Method and Description
Trace<AtomicEvent>	generateTrace(int length) Randomly generates a trace of given length

Methods inherited from class ca.uqac.lif.ecp.GreedyTraceGenerator

generateTraces, getLastCoverage, pickLength, setMaxIterations

Methods inherited from class java.lang.Object

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

Field Detail

m_formula

protected final Operator<AtomicEvent> m_formula

The LTL formula to generate against

m_alphabet

protected final java.util.List<AtomicEvent> m_alphabet

The set of possible events. We store them as a list to make it easier to randomly pick one of them.

Constructor Detail

GreedyLtlGenerator

public GreedyLtlGenerator(Operator<AtomicEvent> op,
                          Alphabet<AtomicEvent> alph,
                          java.util.Random random,
                          CoverageMetric<AtomicEvent,java.lang.Float> metric)

Method Detail

generateTrace

public Trace<AtomicEvent> generateTrace(int length)

Description copied from class: GreedyTraceGenerator

Randomly generates a trace of given length

Specified by:

generateTrace in class GreedyTraceGenerator<AtomicEvent>

Parameters:

length - The length

Returns:

The trace, or null if no trace could be generated