/ONS_Minimise

Minimisation benchmarking code for comparing ONS to NLambda and LOIS

Primary LanguageC++

This repository contains the testing code used to compare ONS to LOIS and NLambda. Each of the subdirectories content can be build by issuing make in the respective subdirectory. This package contains the following:

Automata:
The random automata and structered automata stored in text format.

LOIS:
Testing code for LOIS.
	minimize: Code for minimising automata stored as files. Usage: ./minimize test1.aut test2.aut ...
	fifo, running: Code for generating and then minimising the fifo and ww automata. Usage: ./fifo <n>
	lmax: Code for generating the Lmax sample automaton and minimising it. Usage: ./lmax
	lint: Code for generating the Lint sample automaton and minimising it. Usage: ./lint

NLambda:
Testing code for NLambda.
	minimize: The program for running all examples.
	./minimize File test1.aut test2.aut...  to minimise automata stored as files.
	./minimize Formula test.aut  to minimise a register automaton.
	./minimize Fifo n  to minimise the (non-minimal) fifo example of size n.
	./minimize DoubleWord n  to minimize the ww automaton of size n.
	./minimize Lmax  to minimize the Lmax automaton.
	./minimize Lint  to minimize the Lint automaton.

ONS:
Testing code for ONS, and code for analysing and generating random automata.
	MinimizeTest: Code for minimising automata stored as files. Usage: ./MinimizeTest test1.aut test2.aut ...
	fifo: Code for generating (just generating) fifo automata. Usage: ./fifo <n>
	running: Code for generating (just generating) ww automata. Usage: ./running <n>
	Lmax: Code for generating (just generating) the Lmax sample automaton. Usage: ./Lmax
	Lint: Code for generating (just generating) the Lint sample automaton. Usage: ./Lint
	IsConnected: Test whether the automaton specified by the input file is connected when interpreting the orbits as nodes, and transitions as bidirectional edges. Usage: ./IsConnected test.aut
	GenAutomaton: Generate a random automaton with between N1 and N2 orbits of dimension at most k. Usage: ./GenAutomaton <N1> <N2> <k>
	GenFormulaAutomaton: Generate a random register automaton (with propositions as guards) with n locations, k registers and formula complexity d. Usage: ./GenFormulaAutomaton <N> <k> <d>