Defines the passive methods for automatically learning deterministic finite automata. More...

Namespaces
	CNF
	Contains every method that relies on a SAT solver with CNF clauses.

	NonCNF
	Contains every method that relies on a SAT solver that works on any boolean formula.

	SMT
	Contains every method that relies on a SMT solver.

Classes
class	Method
	The base class of all passive methods. More...

class	MethodFactory
	The Factory Builder design pattern adapted to our methods. More...

class	RegisterInFactory
	Helps to register a method in the factory. More...

Functions
std::unique_ptr< Method >	constructMethod (const std::string &name, unsigned int n, const std::set< std::string > &Sp, const std::set< std::string > &Sm)
	Computes the alphabet and the prefixes set from Sp and Sm and constructs a method for a fixed number of states. More...

std::unique_ptr< Method >	constructMethod (const std::string &name, unsigned int n, const std::set< std::string > &Sp, const std::set< std::string > &Sm, const std::set< std::string > &S, const std::set< std::string > &prefixes, const std::set< char > &alphabet)
	Constructs a method for a fixed number of states. More...

std::pair< std::unique_ptr< Method >, bool >	constructMethod (const std::string &name, const std::set< std::string > &Sp, const std::set< std::string > &Sm, const std::chrono::seconds &timeLimit=std::chrono::seconds(0), long double *timeTaken=nullptr)
	Computes the alphabet and the prefixes set from Sp and Sm and constructs a method with the smallest possible number of states. More...

std::pair< std::unique_ptr< Method >, bool >	constructMethod (const std::string &name, const std::set< std::string > &Sp, const std::set< std::string > &Sm, const std::set< std::string > &S, const std::set< std::string > &prefixes, const std::set< char > &alphabet, const std::chrono::seconds &timeLimit=std::chrono::seconds(0), long double *timeTaken=nullptr)
	Constructs a method with the smallest possible number of states. More...

std::set< std::string >	computeS (const std::set< std::string > &Sp, const std::set< std::string > &Sm)
	Computes $S = S_+ \cup S_-$ . More...

std::set< std::string >	computePrefixes (const std::set< std::string > &S)
	Computes . More...

std::set< char >	computeAlphabet (const std::set< std::string > &S)
	Computes the alphabet $\Sigma$ from the words in . More...

void	readFromFile (const std::string &inputFile, std::set< std::string > &Sp, std::set< std::string > &Sm)
	Reads the and sets from a file. More...

void	generateRandomly (unsigned int numberWords, unsigned int minLength, unsigned int maxLength, unsigned int alphabetSize, std::set< std::string > &Sp, std::set< std::string > &Sm, double SpProbability=0.5)
	Generates randomly a sample set. More...

double	getCPUTime ()

std::unique_ptr< Method >	constructMethodTrigger (const std::string &name, unsigned int n, const std::set< std::string > &Sp, const std::set< std::string > &Sm, const std::set< std::string > &S, const std::set< std::string > &prefixes, const std::set< char > &alphabet, const std::chrono::seconds &timeLimit, std::atomic_bool &stopTrigger, const bool *stopPointer)

Variables
const std::array< const std::string, 8 >	allMethods
	An array with every possible method choice. More...

Detailed Description

Defines the passive methods for automatically learning deterministic finite automata.

These methods receive a sample $S = (S_+, S_-)$ where

is the set of words the automaton must accept
is the set of words the automaton must reject

The words that are not in $S_+$ nor in $S_-$ can be either accepted or rejected (depending on the generated DFA).

Warning: $S_+ \cup S_-$ can not be empty.

Function Documentation

◆ computeAlphabet()

std::set< char > gsjj::passive::computeAlphabet ( const std::set< std::string > & S )

Computes the alphabet $\Sigma$ from the words in $S$ .

Parameters

S The set

Definition at line 27 of file utils.cpp.

◆ computePrefixes()

std::set< std::string > gsjj::passive::computePrefixes ( const std::set< std::string > & S )

Computes $Pref(S)$ .

Parameters

S The set

Definition at line 17 of file utils.cpp.

◆ computeS()

std::set< std::string > gsjj::passive::computeS	(	const std::set< std::string > &	Sp,
		const std::set< std::string > &	Sm
	)

Computes $S = S_+ \cup S_-$ .

In theory, we have $S = (S_+, S_-)$ . However, we need to compute $Pref(S_+, S_-)$ . Therefore, it's easier to have $S = S_+ \cup S_-$ and compute $Pref(S)$ .

Parameters

Sp	The set
Sm	The set

Returns: The set $S = S_+ \cup S_-$

Definition at line 11 of file utils.cpp.

◆ constructMethod() [1/4]

std::unique_ptr< Method > gsjj::passive::constructMethod	(	const std::string &	name,
		unsigned int	n,
		const std::set< std::string > &	Sp,
		const std::set< std::string > &	Sm
	)

Computes the alphabet and the prefixes set from Sp and Sm and constructs a method for a fixed number of states.

Sp and Sm must be disjoint.

Parameters

name	The name of the method to construct
n	The number of states
Sp	The set
Sm	The set

Returns: A method to construct the DFA for the sample

Warning: S can not be empty (and must be coherent with Sp and Sm)

Definition at line 50 of file MethodFactory.cpp.

◆ constructMethod() [2/4]

std::unique_ptr< Method > gsjj::passive::constructMethod	(	const std::string &	name,
		unsigned int	n,
		const std::set< std::string > &	Sp,
		const std::set< std::string > &	Sm,
		const std::set< std::string > &	S,
		const std::set< std::string > &	prefixes,
		const std::set< char > &	alphabet
	)

Constructs a method for a fixed number of states.

Sp and Sm must be disjoint.

Parameters

name	The name of the method to construct
n	The number of states
Sp	The set
Sm	The set
S	The $S = S_+ \cup S_-$ set. See passive::computeS
prefixes	The set. See passive::computePrefixes
alphabet	The alphabet. See computeAlphabet

Returns: A method to construct the DFA for the sample

Warning: S can not be empty (and must be coherent with Sp and Sm)

Definition at line 58 of file MethodFactory.cpp.

◆ constructMethod() [3/4]

std::pair< std::unique_ptr< Method >, bool > gsjj::passive::constructMethod	(	const std::string &	name,
		const std::set< std::string > &	Sp,
		const std::set< std::string > &	Sm,
		const std::chrono::seconds &	timeLimit = `std::chrono::seconds(0)`,
		long double *	timeTaken = `nullptr`
	)

Computes the alphabet and the prefixes set from Sp and Sm and constructs a method with the smallest possible number of states.

This uses a linear search to find the minimal number of states

Sp and Sm must be disjoint.

Parameters

name	The name of the method to construct
Sp	The set
Sm	The set
timeLimit	The time in seconds the program can take to find the best possible method.
timeTaken	If not nullptr, the total time used to solve the different formulas is written. It does NOT give the full CPU time to find the best number of states, juste the time used by the SAT/SMT solvers!

Returns: A method to construct the DFA for the sample and a boolean. The boolean is true iff the function did not reach the time limit.

Warning: S can not be empty (and must be coherent with Sp and Sm)

Definition at line 62 of file MethodFactory.cpp.

◆ constructMethod() [4/4]

std::pair< std::unique_ptr< Method >, bool > gsjj::passive::constructMethod	(	const std::string &	name,
		const std::set< std::string > &	Sp,
		const std::set< std::string > &	Sm,
		const std::set< std::string > &	S,
		const std::set< std::string > &	prefixes,
		const std::set< char > &	alphabet,
		const std::chrono::seconds &	timeLimit = `std::chrono::seconds(0)`,
		long double *	timeTaken = `nullptr`
	)

Constructs a method with the smallest possible number of states.

This uses a linear search to find the minimal number of states

Sp and Sm must be disjoint.

Parameters

name	The name of the method to construct
Sp	The set
Sm	The set
S	$S = S_+ \cup S_-$ . See passive::computeS
prefixes	The set of prefixes of . See passive::computePrefixes
alphabet	The alphabet of . See passive::computeAlphabet
timeLimit	The time in milliseconds the program can take to find the best possible method.
timeTaken	If not nullptr, the total time used to solve the different formulas is written. It does NOT give the full CPU time to find the best number of states, juste the time used by the SAT/SMT solvers!

Returns: A method to construct the DFA for the sample and a boolean. The boolean is true iff the function did not reach the time limit.

Warning: S can not be empty (and must be coherent with Sp and Sm)

Definition at line 70 of file MethodFactory.cpp.

◆ constructMethodTrigger()

std::unique_ptr<Method> gsjj::passive::constructMethodTrigger	(	const std::string &	name,
		unsigned int	n,
		const std::set< std::string > &	Sp,
		const std::set< std::string > &	Sm,
		const std::set< std::string > &	S,
		const std::set< std::string > &	prefixes,
		const std::set< char > &	alphabet,
		const std::chrono::seconds &	timeLimit,
		std::atomic_bool &	stopTrigger,
		const bool *	stopPointer
	)

Definition at line 41 of file MethodFactory.cpp.

◆ generateRandomly()

void gsjj::passive::generateRandomly	(	unsigned int	numberWords,
		unsigned int	minLength,
		unsigned int	maxLength,
		unsigned int	alphabetSize,
		std::set< std::string > &	Sp,
		std::set< std::string > &	Sm,
		double	SpProbability = `0.5`
	)

Generates randomly a sample set.

The alphabet's size is at most 10.

The functions ensures that Sp and Sm do not contain a common word. It must be possible to generate enough words. Otherwise, this function will never terminates.

Parameters

numberWords	The total number of words to generate
minLength	The minimum size of each word
maxLength	The maximum size of each word
alphabetSize	The size of the alphabet. Since symbols are taken randomly in the alphabet, it may happen that a sampling set uses a smaller alphabet.
Sp	The words to accept are put in this set
Sm	The words to reject are put in this set
SpProbability	The probability that a word is put in Sp (by default, 0.5)

Definition at line 54 of file utils.cpp.

◆ getCPUTime()

double gsjj::passive::getCPUTime ( )

Definition at line 81 of file utils.cpp.

◆ readFromFile()

void gsjj::passive::readFromFile	(	const std::string &	inputFile,
		std::set< std::string > &	Sp,
		std::set< std::string > &	Sm
	)

Reads the $S_+$ and $S_-$ sets from a file.

Parameters

inputFile	The path to the file to read
Sp	The set to fill
Sm	The set to fill

Definition at line 37 of file utils.cpp.

Variable Documentation

◆ allMethods

const std::array<const std::string, 8> gsjj::passive::allMethods

Initial value:

= {
            "biermann",
            "unary",
            "binary",
            "heule",
            "neider",
            "unaryNonCNF",
            "binaryNonCNF",
            "heuleNonCNF"
        }

An array with every possible method choice.

Useful to iterate over the methods

Definition at line 26 of file Method.h.

Namespaces

Classes

Functions

Variables

Detailed Description

Function Documentation

◆ computeAlphabet()

◆ computePrefixes()

◆ computeS()

◆ constructMethod() [1/4]

◆ constructMethod() [2/4]

◆ constructMethod() [3/4]

◆ constructMethod() [4/4]

◆ constructMethodTrigger()

◆ generateRandomly()

◆ getCPUTime()

◆ readFromFile()

Variable Documentation

◆ allMethods