Commit 66143ffe authored by Tereza Kinská's avatar Tereza Kinská
Browse files

fix argparse name argument

parent 825c86ff

src/algorithm/algorithm.cpp

+2 −16
Original line number Diff line number Diff line
@@ -231,21 +231,6 @@ std::optional<Witness> runAlgorithm(const BuchiMatrix &u, const BuchiMatrix &v, 
	const int number_of_matrices, spot::twa_graph_ptr &automaton, std::vector<unsigned int> &accepting_states) {

	int epsilonValues[4] = {0, 0, 0, 0};



	std::cout << "Running algorithm with matrices: " << std::endl;

	std::cout << "u: " << std::endl;

	u.print();

	std::cout << "v: " << std::endl;

	v.print();

	std::cout << "w: " << std::endl;

	w.print();

	std::cout << "x: " << std::endl;

	x.print();

	std::cout << "y: " << std::endl;

	y.print();

	std::cout << "z: " << std::endl;

	z.print();

	std::cout << std::endl;



	for (int i=0; i<4; ++i) {

		epsilonValues[i] = 1;

		if (i>0) {
@@ -281,6 +266,7 @@ std::optional<Witness> runAlgorithm(const BuchiMatrix &u, const BuchiMatrix &v, 
	}



	return {}; // Is LTL-definable

	// return std::nullopt; // Is LTL-definable

}
@@ -426,7 +412,7 @@ unsigned int getMaxWordLength(int number_of_states, int accepting_states_count) 
unsigned int getMaxIndexWords(unsigned int max_word_length, unsigned int alphabet_size) {

	unsigned int max_index = 0;

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

		max_index += alphabet_size^i;

		max_index += pow(alphabet_size, i);

	}

	return max_index;

}

src/data_structures/data_structures.cpp

+0 −10
Original line number Diff line number Diff line
@@ -215,13 +215,6 @@ BuchiMatrix BuchiMatrix::computeMatrixPowerBinary(const unsigned int power) cons 
 * @returns product these matrices.

 */

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

	std::cout << "Multiplying matrices..." << std::endl;

	std::cout << "Matrix size A: " << mMatrixSize << ", Matrix size B: " << otherMatrix.getSize() << std::endl;

	std::cout << "Matrix A: " << std::endl;

	this->print();

	std::cout << "Matrix B: " << std::endl;

	otherMatrix.print();

	std::cout << std::endl;

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

	assert(this->getSize() == otherMatrix.getSize());
@@ -237,9 +230,6 @@ BuchiMatrix BuchiMatrix::multiplyWithMatrix(const BuchiMatrix &otherMatrix) cons 
		}

	}



	std::cout << "Resulting matrix: " << std::endl;

	resultMatrix.print();

	std::cout << std::endl;

	return resultMatrix;

}

src/data_structures/iterators.cpp

+0 −3
Original line number Diff line number Diff line
@@ -100,8 +100,6 @@ std::vector<spot::formula> WordIterator::getWordFromIndex(unsigned int index) co 
	std::vector<spot::formula> word;

	unsigned int current_index = index;

	

	assert(index <= pow(alphabet_size, max_word_length));

	

	while (current_index > 0) {

		current_index -= 1;

		spot::formula letter = alphabet[current_index % alphabet_size];
@@ -125,7 +123,6 @@ std::vector<unsigned int> WordIterator::getWordIndexesFromIndex(unsigned int wor 
	std::vector<unsigned int> word_indexes;

	unsigned int current_word_index = word_index;

	

	assert(word_index <= pow(alphabet_size, max_word_length));



	while (current_word_index > 0) {

		current_word_index -= 1;

src/data_structures/witness.cpp

+4 −4
Original line number Diff line number Diff line
@@ -17,8 +17,8 @@ Witness::Witness() { 
/**

 * Constructor for the Witness class without given automaton name.

 */

Witness::Witness(const vector<BuchiMatrix> wordMatrices, 

							const std::vector<std::vector<spot::formula>> wordValues, 

Witness::Witness(const vector<BuchiMatrix> &wordMatrices, 

							const std::vector<std::vector<spot::formula>> &wordValues, 

							unsigned int epsilonOneIndex) 

							: Witness(wordMatrices, wordValues, epsilonOneIndex, "without name") {}
@@ -26,8 +26,8 @@ Witness::Witness(const vector<BuchiMatrix> wordMatrices, 
/**

 * Constructor for the Witness class setting everything.

 */

Witness::Witness(const vector<BuchiMatrix> wordMatrices, 

							const std::vector<std::vector<spot::formula>> wordValues, 

Witness::Witness(const vector<BuchiMatrix> &wordMatrices, 

							const std::vector<std::vector<spot::formula>> &wordValues, 

							unsigned int epsilonOneIndex, std::string automaton_name) {

	mWordMatrices = wordMatrices;

	mWords = wordValues;

src/data_structures/witness.hpp

+2 −2
Original line number Diff line number Diff line
@@ -19,8 +19,8 @@ class Witness { 
	// Methods

	public:

		Witness();

		Witness(const vector<BuchiMatrix> wordMatrices, const std::vector<std::vector<spot::formula>> wordValues, unsigned int epsilonOneIndex);

		Witness(const vector<BuchiMatrix> wordMatrices, const std::vector<std::vector<spot::formula>> wordValues, unsigned int epsilonOneIndex, std::string automaton_name);

		Witness(const vector<BuchiMatrix> &wordMatrices, const std::vector<std::vector<spot::formula>> &wordValues, unsigned int epsilonOneIndex);

		Witness(const vector<BuchiMatrix> &wordMatrices, const std::vector<std::vector<spot::formula>> &wordValues, unsigned int epsilonOneIndex, std::string automaton_name);



		std::vector<BuchiMatrix> getWordMatrices() const;

		std::vector<std::vector<spot::formula>> getWords() const;