/**-------------------------------------------------------------------
 * Program for checking Petri net solvability/unsolvability of       *
 * binary words. Implementation based on pattern matching condition  *
 * and the algorithm presented in the paper:                         *
 *                                                                   *
 * E.Erofeev, K. Barylska, Ł. Mikulski, M. Piątkowski                *
 * "Generating All Minimal Petri Net Unsolvable Binary Words"        *
 * Proc. of Prague Stringology Conference 2016                       *
 *                                                                   *
 * (c) 2016, Marcin Piątkowswki, marcin.piatkowski@mat.umk.pl        *
 *-------------------------------------------------------------------*/

#include <iostream>
#include <string>
#include <vector>

using namespace std;


/** Checks the existence of a factor of the form
 * 'abw (baw)^k a' or 'baw (abw)^k b'
 * in wrd starting from the position pos.
 */
bool findPrefixRun(const string &wrd, int pos, char tr) { /* O(n) */
	vector<int> bord(wrd.length()+1);
	int t = bord[0] = 0;

	// Compute border array
	for(unsigned pp=pos+1;pp<wrd.length()-1;++pp) {
		while(t>0 && wrd[pos+t]!=wrd[pp]) {
			t = bord[t-1];
		}

		if(wrd[pos+t]==wrd[pp]) {
			++t;
		}

		bord[pp-pos] = t;
		
		// Found an occurrence of 'abw (baw)^k a' or 'baw (abw)^k b' ending at position pp		
		if((bord[pp-pos]>2) && ((pp-pos+1)%(pp-pos-bord[pp-pos]+1)==0) && wrd[pp+1]==tr)
			return true;
	}
	
	return false;
}


/** Checks whether wrd is PN-solvable using pattern matching criteria */
bool checkBinarySolvability(string wrd) {
	wrd.append("$");
	
	/* Scan wrd from right to left marking positions of a's and b's.
	 * Return false if factor of the form
	 * 'a b^j a b^k a' or 'b a^j b a^k b' (j>=k+1, k>=0) 
	 * was found */
	int lastA = -1, lastLastA = -1, lastB = -1, lastLastB = -1, numA = 0, numB = 0;
	
	for(int pos=wrd.length()-2;pos>=0;--pos) {  /* O(n) */
		switch(wrd[pos]) {
			case 'a':
				++numA;

				/* An occurrence of a factor "a b b^j b^k a b^j a" */
				if(numA>2 && lastA-pos>lastLastA-lastA+1)
					return false;
				
				lastLastA = lastA;
				lastA = pos;
				break;
				
			case 'b':
				++numB;
				
				/* An occurrence of a factor "b a a^j a^k b a^j b" */
				if(numB>2 /*&& lastB!=-1 && lastLastB!=-1*/ && lastB-pos>lastLastB-lastB+1)
					return false;
				
				lastLastB = lastB;
				lastB = pos;
				break;
				
			default:
				return false; // wrd is not a binary string
		}
	}
	
	/* For each occurrence of 'ab' and 'ba' in wrd: 
	 *     - switch  a <--> b
	 *     - compute repetition aware border array
	 *     - look for a factor of the form 'abw (baw)^k a' or 'baw (abw)^k b'
	 *       for each possible starting position
	 */
	for(int pos=0;pos<wrd.length()-5;++pos) { /* O(n^2) */
		if(wrd[pos]=='a' && wrd[pos+1]=='b') {
			swap(wrd[pos],wrd[pos+1]);
			
			if(findPrefixRun(wrd,pos,'a')) /* O(n) */
				return false;
			
			swap(wrd[pos],wrd[pos+1]);
		}
		else if(wrd[pos]=='b' && wrd[pos+1]=='a') {
			swap(wrd[pos],wrd[pos+1]);
			
			if(findPrefixRun(wrd,pos,'b')) /* O(n) */
				return false;
			
			swap(wrd[pos],wrd[pos+1]);
		}
	}
	
	return true;
}


/** Checks whether wrd consists of a's and b's only */
bool isBinary(string wrd) {
	for(unsigned i=0;i<wrd.length();++i)
		if(wrd[i]!='a' && wrd[i]!='b')
			return false;
			
	return true;
}


int main(int argc, char **argv) {

	if(argc==1) {
		cerr << "Usage: " << argv[0] << " list_of_words" << endl;
		
		return 1;
	}
	
	for(int i=1;i<argc;++i) {
		if(!isBinary(argv[i])) {
			cout << argv[i] << " - not binary" << endl;
			continue;
		}
		
		if(checkBinarySolvability(argv[i]))
			cout << argv[i] << " - solvable" << endl;
		else
			cout << argv[i] << " - unsolvable" << endl;
	}
	
	return 0;
}