Package modelcounter

Class AutomataBasedModelCounting

java.lang.Object

modelcounter.AutomataBasedModelCounting

public class AutomataBasedModelCounting
extends Object

Field Summary

Fields

Modifier and Type	Field	Description
static int	TIMEOUT

Constructor Summary

Constructors

Constructor	Description
AutomataBasedModelCounting(gov.nasa.ltl.graph.Graph<String> input_graph, boolean exhaustive)
AutomataBasedModelCounting(owl.ltl.LabelledFormula formula, boolean exhaustive)

Method Summary

Modifier and Type	Method	Description
org.ejml.data.DMatrixRMaj	buildTransferMatrix(gov.nasa.ltl.graph.Graph<String> nba)	Build the Transfer Matrix for the given DFA
BigInteger	count(int k)

Methods inherited from class java.lang.Object

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

Field Detail

TIMEOUT

public static int TIMEOUT

Constructor Detail

AutomataBasedModelCounting

public AutomataBasedModelCounting(owl.ltl.LabelledFormula formula,
                                  boolean exhaustive)

AutomataBasedModelCounting

public AutomataBasedModelCounting(gov.nasa.ltl.graph.Graph<String> input_graph,
                                  boolean exhaustive)

Method Detail

count

public BigInteger count(int k)

buildTransferMatrix

public org.ejml.data.DMatrixRMaj buildTransferMatrix(gov.nasa.ltl.graph.Graph<String> nba)

Build the Transfer Matrix for the given DFA

Parameters:

nba - is the DFA

Returns:

a n x n matrix M where M[i,j] is the number of transitions from state si to state sj