Package modelcounter

Class MatrixBigIntegerModelCounting

java.lang.Object

modelcounter.MatrixBigIntegerModelCounting

public class MatrixBigIntegerModelCounting
extends Object

Constructor Summary

Constructors

Constructor	Description
MatrixBigIntegerModelCounting(owl.ltl.LabelledFormula formula, boolean exhaustive)

Method Summary

Modifier and Type	Method	Description
org.apache.commons.math3.linear.FieldMatrix<org.apache.commons.math3.fraction.BigFraction>	buildTransferMatrix(gov.nasa.ltl.graph.Graph<String> nba)	Build the Transfer Matrix for the given DFA
BigInteger	count(int k)
org.apache.commons.math3.linear.FieldMatrix<org.apache.commons.math3.fraction.BigFraction>	createMatrix(int row, int column)

Methods inherited from class java.lang.Object

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

Constructor Detail

MatrixBigIntegerModelCounting

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

Method Detail

count

public BigInteger count(int k)

buildTransferMatrix

public org.apache.commons.math3.linear.FieldMatrix<org.apache.commons.math3.fraction.BigFraction> 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

createMatrix

public org.apache.commons.math3.linear.FieldMatrix<org.apache.commons.math3.fraction.BigFraction> createMatrix(int row,
                                                                                                               int column)