Commit a1ed33e7 authored by Tereza Kinská's avatar Tereza Kinská
Browse files

refactoring - arrays to vectors in matrix iterator

parent 5acb8de9

src/algorithm/algorithm.cpp

+11 −13
Original line number Diff line number Diff line
@@ -47,7 +47,7 @@ std::optional<Witness> isLtlDefinableAllMatricesLazy(spot::twa_graph_ptr &automa 
		y.fillByIndex(matrix_iterators[4].getIndex());

		z.fillByIndex(matrix_iterators[5].getIndex());



		std::optional<Witness> found_witness = runAlgorithm(u, v, w, x, y, z, number_of_matrices, automaton, accepting_states);

		std::optional<Witness> found_witness = runAlgorithm(u, v, w, x, y, z, number_of_matrices, automaton);

		if (found_witness) {



			// Check for spuriousness of the witness
@@ -132,7 +132,7 @@ std::optional<Witness> isLtlDefinableAllMatricesEager(spot::twa_graph_ptr &autom 
		// Check for spuriousness of the witness

		if (areMatricesReal(u, v, w, x, y, z, mata_matrix, number_of_states, words, automaton->get_dict())) {

			

			std::optional<Witness> found_witness = runAlgorithm(u, v, w, x, y, z, number_of_matrices, automaton, accepting_states);

			std::optional<Witness> found_witness = runAlgorithm(u, v, w, x, y, z, number_of_matrices, automaton);

			if (found_witness) {

				Witness witness = found_witness.value();

				witness.setWords(words);
@@ -218,7 +218,7 @@ std::optional<Witness> isLtlDefinableAllWords(spot::twa_graph_ptr &automaton) { 
		y.fillByWordIndicesFromAlphabet(words_indices[4], alphabet_matrices);

		z.fillByWordIndicesFromAlphabet(words_indices[5], alphabet_matrices);



		std::optional<Witness> possible_witness = runAlgorithm(u, v, w, x, y, z, number_of_matrices, automaton, accepting_states);

		std::optional<Witness> possible_witness = runAlgorithm(u, v, w, x, y, z, number_of_matrices, automaton);

		

		if (possible_witness.has_value()) {

			Witness witness = possible_witness.value();
@@ -270,7 +270,7 @@ std::optional<Witness> isLtlDefinableAllWords(spot::twa_graph_ptr &automaton) { 
 * 			empty optional if the automaton is LTL-definable

 */

std::optional<Witness> runAlgorithm(const BuchiMatrix &u, const BuchiMatrix &v, const BuchiMatrix &w, const BuchiMatrix &x, const BuchiMatrix &y, const BuchiMatrix &z, 

	const int number_of_matrices, spot::twa_graph_ptr &automaton, std::vector<unsigned int> &accepting_states) {

	const int number_of_matrices, spot::twa_graph_ptr &automaton) {

	// v^m, y^m, v^(m+1), y^(m+1)

	BuchiMatrix v_to_m = v.computeMatrixPowerBinary(number_of_matrices);

	BuchiMatrix y_to_m = y.computeMatrixPowerBinary(number_of_matrices);
@@ -287,9 +287,9 @@ std::optional<Witness> runAlgorithm(const BuchiMatrix &u, const BuchiMatrix &v, 


	// Check for inverse image in language

	// We want combinations s,e,s,e_plus_1   and   s,e,s_plus_1,e

	bool isFstInLanguage = isInverseInLanguage(s, e, automaton, accepting_states);

	bool isSndInLanguage = isInverseInLanguage(s, e_plus_1, automaton, accepting_states);

	bool isTrdInLanguage = isInverseInLanguage(s_plus_1, e, automaton, accepting_states);

	bool isFstInLanguage = isInverseInLanguage(s, e, automaton);

	bool isSndInLanguage = isInverseInLanguage(s, e_plus_1, automaton);

	bool isTrdInLanguage = isInverseInLanguage(s_plus_1, e, automaton);





	// Found witness?
@@ -335,8 +335,8 @@ bool areMatricesReal(const BuchiMatrix &u, const BuchiMatrix &v, const BuchiMatr 
			for (unsigned q = 0; q < number_of_states; ++q) {

				//mata::nfa::Nfa current_nfa = (m.at(p, q) == INF) ? mata_matrix.getInfNfaAt(p, q) : mata_matrix.getOneNfaAt(p, q);

				switch (m.at(p, q)) {

						case INF: current_nfa = mata_matrix.getInfNfaAt(p, q);

						case ONE: current_nfa = mata_matrix.getOneNfaAt(p, q);

						case INF: current_nfa = mata_matrix.getInfNfaAt(p, q); break;

						case ONE: current_nfa = mata_matrix.getOneNfaAt(p, q); break;

						// default means ZERO, other options are not possible

						// complements using only symbols already in the automaton. There must be a letter usage in input ba to have it in the witness

						default: current_nfa = mata_matrix.getCoReachNfaAt(p, q);
@@ -399,7 +399,7 @@ bool checkReachedAccState(const BuchiMatrix &m, unsigned int init_state, std::ve 
/**

 * Check whether the whole inverse image of se^omega is subsumed in the language.

 */

bool isInverseInLanguage(const BuchiMatrix &s, const BuchiMatrix &e, spot::twa_graph_ptr &automaton, std::vector<unsigned int> &accepting_states) {

bool isInverseInLanguage(const BuchiMatrix &s, const BuchiMatrix &e, spot::twa_graph_ptr &automaton) {

	unsigned int init_state = automaton->get_init_state_number();

	unsigned int number_of_states = automaton->num_states();
@@ -507,8 +507,6 @@ unsigned long long getMaxWordLength(int number_of_states, int accepting_states_c 




unsigned long long getMaxIndexWords(unsigned long long max_word_length, unsigned int alphabet_size) {	

	std::cout << "maximal word length: " << max_word_length << std::endl;

	

	unsigned long long max_index = 0;

	//unsigned int division_ratio = safe_pow(alphabet_size, 4);

src/algorithm/algorithm.hpp

+9 −9
Original line number Diff line number Diff line 
#pragma once



#include <cassert>

#include <cmath>

//#include <cassert>

//#include <cmath>

#include <optional>



#include <spot/tl/simplify.hh>

#include <spot/twa/twagraph.hh>

#include <mata/nfa/nfa.hh>

//#include <spot/tl/simplify.hh>

//#include <spot/twa/twagraph.hh>

//#include <mata/nfa/nfa.hh>





#include "../data_structures/data_structures.hpp"

#include "../data_structures/witness.hpp"

//#include "../data_structures/data_structures.hpp"

#include "../data_structures/iterators.hpp"

#include "../data_structures/witness.hpp"



std::optional<Witness> isLtlDefinableAllMatricesLazy(spot::twa_graph_ptr &automaton);

std::optional<Witness> isLtlDefinableAllMatricesEager(spot::twa_graph_ptr &automaton);
@@ -19,10 +19,10 @@ std::optional<Witness> isLtlDefinableAllMatricesEager(spot::twa_graph_ptr &autom 
std::optional<Witness> isLtlDefinableAllWords(spot::twa_graph_ptr &automaton);



std::optional<Witness> runAlgorithm(const BuchiMatrix &u, const BuchiMatrix &v, const BuchiMatrix &w, const BuchiMatrix &x, const BuchiMatrix &y, const BuchiMatrix &z, 

	const int number_of_matrices, spot::twa_graph_ptr &automaton, std::vector<unsigned int> &accepting_states);

	const int number_of_matrices, spot::twa_graph_ptr &automaton);



bool areMatricesReal(const BuchiMatrix &u, const BuchiMatrix &v, const BuchiMatrix &w, const BuchiMatrix &x, const BuchiMatrix &y, const BuchiMatrix &z, 

		MataNfaMatrix &mata_matrix, unsigned number_of_states, std::vector<std::vector<spot::formula>> &words, const spot::bdd_dict_ptr& dict);

bool isInverseInLanguage(const BuchiMatrix &s, const BuchiMatrix &e, spot::twa_graph_ptr &automaton, std::vector<unsigned int> &accepting_states);

bool isInverseInLanguage(const BuchiMatrix &s, const BuchiMatrix &e, spot::twa_graph_ptr &automaton);

unsigned long long getMaxWordLength(int number_of_states, int accepting_states_count);

unsigned long long getMaxIndexWords(unsigned long long max_word_length, unsigned int alphabet_size);
 
 No newline at end of file

src/data_structures/data_structures.cpp

+48 −26
Original line number Diff line number Diff line
@@ -8,9 +8,10 @@ using namespace spot; 
 * Neutral element for Buchi matrix is a matrix of ONEs.

 */

BuchiMatrix::BuchiMatrix(const unsigned int size) 

	: mMatrixSize(size), data(new BuchiValue[size * size])  // Correct initialization order

	: mMatrixSize(size)//, data(new BuchiValue[size * size])  // Correct initialization order

	{

	// Default/neutral value

	data.reserve(size * size);

	makeIdentity();

}
@@ -19,9 +20,10 @@ BuchiMatrix::BuchiMatrix(const unsigned int size) 
 * Sets the matrix to the identity matrix.

 */

void BuchiMatrix::makeIdentity() {

	std::fill_n(data, mMatrixSize * mMatrixSize, ZERO);

	//std::fill_n(data, mMatrixSize * mMatrixSize, ZERO);

	data.assign(mMatrixSize * mMatrixSize, ZERO);

	for (unsigned int i=0; i < mMatrixSize; ++i) {

		at(i, i) = ONE; // neutral element for multiplication

		set(i, i, ONE); // neutral element for multiplication

	}

}
@@ -31,10 +33,11 @@ void BuchiMatrix::makeIdentity() { 
 * 

 * Note: Too big @param word_index is fine, the function will just fill the matrix with INFs.

 */

BuchiMatrix::BuchiMatrix(const unsigned int size, const unsigned int matrix_index) 

	: mMatrixSize(size), data(new BuchiValue[size * size])  // Correct initialization order

BuchiMatrix::BuchiMatrix(const unsigned int size, const unsigned long long matrix_index) 

	: mMatrixSize(size)//, data(new BuchiValue[size * size])  // Correct initialization order

	{

	//std::fill_n(data, mMatrixSize * mMatrixSize, ZERO);

	data.reserve(size * size);

	fillByIndex(matrix_index);

}
@@ -43,26 +46,29 @@ BuchiMatrix::BuchiMatrix(const unsigned int size, const unsigned int matrix_inde 
 * Fills the matrix with values according to the given index.

 * The index is a number in the range [0, 3^(size^2)-1].

 */

void BuchiMatrix::fillByIndex(const unsigned int matrix_index) {

	unsigned int index = matrix_index;

void BuchiMatrix::fillByIndex(const unsigned long long matrix_index) {

	unsigned long long index = matrix_index;

	for (unsigned int i=0; i < mMatrixSize; ++i) {

		for (unsigned int j=0; j < mMatrixSize; ++j) {

			if (index % 3 == 0) {

				at(i, j) = ZERO;

				set(i, j, ZERO);

			} else if (index % 3 == 1) {

				at(i, j) = ONE;

				set(i, j, ONE);

			} else {

				at(i, j) = INF;

				set(i, j, INF);

			}

			index /= 3;

		}

	}

}



BuchiMatrix::BuchiMatrix(const unsigned int size, spot::twa_graph_ptr &automaton, const spot::formula letter) : mMatrixSize(size), data(new BuchiValue[size * size]) {

BuchiMatrix::BuchiMatrix(const unsigned int size, spot::twa_graph_ptr &automaton, const spot::formula letter) 

						: mMatrixSize(size)//, data(new BuchiValue[size * size]) 

{

	std::vector<bool> is_acc_state;

	getAcceptingStatesBool(is_acc_state, automaton);



	data.reserve(size * size);

	fillByLetter(automaton, letter, is_acc_state);

}
@@ -70,16 +76,17 @@ BuchiMatrix::BuchiMatrix(const unsigned int size, spot::twa_graph_ptr &automaton 
void BuchiMatrix::fillByLetter(spot::twa_graph_ptr &automaton, const spot::formula letter, std::vector<bool> &is_acc_state) {

	const spot::bdd_dict_ptr& dict = automaton->get_dict();

	

	std::fill_n(data, mMatrixSize * mMatrixSize, ZERO);

	//std::fill_n(data, mMatrixSize * mMatrixSize, ZERO);

	data.assign(mMatrixSize * mMatrixSize, ZERO);

	for (unsigned int state=0; state < mMatrixSize; ++state) {

		BuchiValue value = is_acc_state[state] ? INF : ONE;



		for (auto& e: automaton->out(state)) {

			if (isSubsumed(letter, spot::bdd_to_formula(e.cond, dict), dict)) {

				if (value == INF) {

					at(state, e.dst) = INF;

					set(state, e.dst, INF);

				} else {

					at(state, e.dst) = is_acc_state[e.dst] ? INF : ONE;

					set(state, e.dst, is_acc_state[e.dst] ? INF : ONE);

				}

			}

		}
@@ -109,20 +116,32 @@ void matrix_initialization_dfs(spot::twa_graph_ptr aut, unsigned state, std::vec 
 * Fills the matrix according to the given @param automaton and @param word.

 */

BuchiMatrix::BuchiMatrix(const unsigned int size, spot::twa_graph_ptr &automaton, const std::vector<spot::formula> &word) 

	: mMatrixSize(size), data(new BuchiValue[size * size])  // Correct initialization order

	: mMatrixSize(size)//, data(new BuchiValue[size * size])  // Correct initialization order

	{

	// neutral element, no IFTs for no letters

	std::fill_n(data, mMatrixSize * mMatrixSize, ZERO);

	for (unsigned int i=0; i < mMatrixSize; ++i) { at(i, i) = ONE; }

	//std::fill_n(data, mMatrixSize * mMatrixSize, ZERO);

	//data.assign(mMatrixSize * mMatrixSize, ZERO);

	//for (unsigned int i=0; i < mMatrixSize; ++i) { at(i, i) = ONE; }

	data.reserve(size * size);

	makeIdentity();



	// TODO add optimise

	//std::vector<bool> is_acc_state;

	//getAcceptingStatesBool(is_acc_state, automaton);



	//BuchiMatrix letter_matrix = BuchiMatrix(size);

	for (spot::formula letter : word) {

		//letter_matrix.fillByLetter(automaton, letter, is_acc_state);

		*this = multiplyWithMatrix(BuchiMatrix(size, automaton, letter));

	}

}





BuchiMatrix::BuchiMatrix(const unsigned int size, const std::vector<unsigned int> &word_indices, AlphabetMatrices &alphabet_matrices) 

		: mMatrixSize(size), data(new BuchiValue[size * size]) { // Correct initialization order

		: mMatrixSize(size)//, data(new BuchiValue[size * size]) { // Correct initialization order

{

	data.reserve(size * size);

	data.assign(mMatrixSize * mMatrixSize, ZERO);

	fillByWordIndicesFromAlphabet(word_indices, alphabet_matrices);

}
@@ -156,7 +175,7 @@ unsigned int BuchiMatrix::getElemsCount() const { 
 * 

 * @returns pointer to value at given coordinates.

 */

BuchiValue& BuchiMatrix::at(const unsigned int x, const unsigned int y) const {

BuchiValue BuchiMatrix::at(const unsigned int x, const unsigned int y) const {

	if((x > mMatrixSize) || (y > mMatrixSize)) {

		throw std::out_of_range("Matrix coordinates out of range.");

	}
@@ -185,14 +204,14 @@ void BuchiMatrix::set(const unsigned int x, const unsigned int y, const BuchiVal 
 * 

 * @return @this matric to the power of @param power.

 */

BuchiMatrix BuchiMatrix::computeMatrixPowerIterative(const unsigned int power) const {

BuchiMatrix BuchiMatrix::computeMatrixPowerIterative(const unsigned long long power) const {

	BuchiMatrix resultingMatrix = BuchiMatrix(this->getSize());

	

	if (power == 0) { // neutral element, no INFs for no letters

		return resultingMatrix;

	}



	for (unsigned int i=1; i <= power; ++i) {

	for (unsigned long long i=1; i <= power; ++i) {

		resultingMatrix = resultingMatrix.multiplyWithMatrix(*this);

	}
@@ -206,9 +225,9 @@ BuchiMatrix BuchiMatrix::computeMatrixPowerIterative(const unsigned int power) c 
 * 

 * @return @this matric to the power of @param power.

 */

BuchiMatrix BuchiMatrix::computeMatrixPowerBinary(const unsigned int power) const {

BuchiMatrix BuchiMatrix::computeMatrixPowerBinary(const unsigned long long power) const {

	BuchiMatrix resultMatrix = BuchiMatrix(this->getSize());

	unsigned int remainingExponent = power;

	unsigned long long remainingExponent = power;

	BuchiMatrix base_matrix = *this;



	while (remainingExponent > 0) {
@@ -230,6 +249,9 @@ BuchiMatrix BuchiMatrix::computeMatrixPowerBinary(const unsigned int power) cons 
 * @returns product these matrices.

 */

BuchiMatrix BuchiMatrix::multiplyWithMatrix(const BuchiMatrix &otherMatrix) const {

	if (this->getSize() > std::numeric_limits<unsigned int>::max() / this->getSize()) {

    	throw std::overflow_error("BuchiMatrix size too large!");

	}

	BuchiMatrix resultMatrix = BuchiMatrix(this->getSize());

	assert(this->getSize() == otherMatrix.getSize());
@@ -241,7 +263,7 @@ BuchiMatrix BuchiMatrix::multiplyWithMatrix(const BuchiMatrix &otherMatrix) cons 
						new_value = addBuchiValues(new_value, multiplyBuchiValues(at(iThis, k), otherMatrix.at(k, jThis)));

					}

				}

			resultMatrix.at(iThis, jThis) = new_value;

			resultMatrix.set(iThis, jThis, new_value);

		}

	}
@@ -304,12 +326,12 @@ BuchiValue addBuchiValues(const BuchiValue buchiValue1, const BuchiValue buchiVa 
 */

void BuchiMatrix::MultiplyWithBuchiValue(const BuchiValue multiplier) {

	switch (multiplier) {

		case ZERO: std::fill_n(data, mMatrixSize*mMatrixSize, ZERO);

		case ZERO: data.assign(mMatrixSize * mMatrixSize, ZERO); break;

		case ONE: break;

		case INF: for (unsigned int i=0; i < mMatrixSize; ++i) {

					for (unsigned int j=0; j < mMatrixSize; ++j) {

						if (at(i, j) == ONE) {

							at(i, j) = INF;

							set(i, j, INF);

						}

					}

				}

src/data_structures/data_structures.hpp

+7 −6
Original line number Diff line number Diff line
@@ -44,29 +44,30 @@ class BuchiMatrix { 


	public:

		//BuchiValue *data[mMatrixSize][mMatrixSize] = new BuchiValue[mMatrixSize * mMatrixSize];

		BuchiValue *data; //= new BuchiValue[mMatrixSize * mMatrixSize];

		//BuchiValue *data; //= new BuchiValue[mMatrixSize * mMatrixSize];

		std::vector<BuchiValue> data;



	// Methods

	public:

		BuchiMatrix(const unsigned int size);

		BuchiMatrix(const unsigned int size, const unsigned int word_index);

		BuchiMatrix(const unsigned int size, const unsigned long long word_index);

		BuchiMatrix(const unsigned int size, spot::twa_graph_ptr &automaton, const spot::formula letter);

		BuchiMatrix(const unsigned int size, spot::twa_graph_ptr &automaton, const std::vector<spot::formula> &word);

		BuchiMatrix(const unsigned int size, const std::vector<unsigned int> &word_indices, AlphabetMatrices &alphabet_matrices);

		

		void makeIdentity();

		void fillByIndex(const unsigned int matrix_index);

		void fillByIndex(const unsigned long long matrix_index);

		void fillByLetter(spot::twa_graph_ptr &automaton, const spot::formula letter, std::vector<bool> &is_acc_state);

		void fillByWordIndicesFromAlphabet(const std::vector<unsigned int> &word_indices, AlphabetMatrices &alphabet_matrices);



		unsigned int getSize() const;

		unsigned int getElemsCount() const;

		BuchiValue& at(const unsigned int x, const unsigned int y) const;

		BuchiValue at(const unsigned int x, const unsigned int y) const;

		void set(const unsigned int x, const unsigned int y, const BuchiValue value);

		bool operator==(const BuchiMatrix &otherMatrix) const;



		BuchiMatrix computeMatrixPowerIterative(const unsigned int power) const;

		BuchiMatrix computeMatrixPowerBinary(const unsigned int power) const;

		BuchiMatrix computeMatrixPowerIterative(const unsigned long long power) const;

		BuchiMatrix computeMatrixPowerBinary(const unsigned long long power) const;

		BuchiMatrix multiplyWithMatrix(const BuchiMatrix &otherMatrix) const;

		void MultiplyWithBuchiValue(const BuchiValue multiplier);

src/data_structures/iterators.cpp

+14 −6
Original line number Diff line number Diff line
@@ -6,7 +6,8 @@ 
WordIterator::WordIterator(std::vector<spot::formula> atomic_propositions, unsigned long long max_word_length, std::vector<unsigned int> accepting_states, unsigned int number_of_states) 

	: max_word_length(max_word_length), index(1) {

	alphabet = getLetters(atomic_propositions);

	this->isAccepting = new bool[number_of_states];

	//this->isAccepting = new bool[number_of_states];

	isAccepting.resize(number_of_states);

	for (unsigned int i = 0; i < number_of_states; ++i) {

		this->isAccepting[i] = false;

	}
@@ -18,22 +19,29 @@ WordIterator::WordIterator(std::vector<spot::formula> atomic_propositions, unsig 




/**

 * Returns the alphabet of @param automaton, i.e. the powerset of all atomic propositions.

 * Returns the alphabet of the automaton, i.e. the powerset of all atomic propositions @param atomic_propositions.

 */

std::vector<formula> WordIterator::getLetters(std::vector<spot::formula> atomic_propositions) {

std::vector<formula> WordIterator::getLetters(const std::vector<spot::formula> atomic_propositions) {

	unsigned int ap_count = atomic_propositions.size();



	std::vector<spot::formula> letters;

	//spot::formula f;

	for (unsigned int i = 0; i < pow(2, ap_count); i++) {

		spot::formula f = spot::formula::tt();

		unsigned int current = i;

		for (unsigned int j = 0; j < ap_count; j++) {

			spot::formula new_prop = atomic_propositions[j];

			//spot::formula new_prop = atomic_propositions[j];

			spot::formula new_prop = spot::formula(atomic_propositions[j]);

			if (current % 2 == 1) {

				new_prop = spot::formula::Not(new_prop);

			}

			std::vector<spot::formula> formulae = {f, new_prop};

			f = spot::formula::And(formulae);

			//std::vector<spot::formula> formulae; // = {f, new_prop};

			//formulae.push_back(f);

			//formulae.push_back(new_prop);

			//f = spot::formula::And(formulae);

			spot::formula tmp_f = f;

			std::vector<spot::formula> conjuncts = {tmp_f, new_prop};

			f = spot::formula::And(conjuncts);

			current /= 2;

		}