#define SIZE 4
#define MAX 4

typedef array{
        byte aa[SIZE];
}

byte arr1[SIZE];
byte arr2[SIZE];
array finalarray[SIZE];
byte m = SIZE;
byte n = SIZE;


inline initArray1()
{
   i = 0;
   do
   :: (i>=SIZE) -> break;
   :: else ->
      v = 0;
      do
      :: (v >= 0) -> break;
      :: (v < MAX) -> v++;
      od;
      arr1[i] = v;
      i++;
   od;
}

inline initArray2()
{
   i = 0;
   do
   :: (i>=SIZE) -> break;
   :: else ->
      v = 0;
      do
      :: (v >= 0) -> break;
      :: (v < MAX) -> v++;
      od;
      arr2[i] = v;
      i++;
   od;
}

inline LCSsubstr(){
    i = 0;
    result = 0;
    do
    :: (i >= SIZE) -> break;
    :: else ->
       j = 0;
       do
       :: (j >= SIZE) -> break;
       ::else ->
        if
        :: (i == 0 || j == 0) -> finalarray[i].aa[j] = 0;
        ::else ->
            if
            :: (arr1[i - 1] == arr2[j - 1]) ->
                finalarray[i].aa[j] = finalarray[i-1].aa[j-1] + 1;
                if
                :: (finalarray[i].aa[j] > result) -> result = finalarray[i].aa[j];
                fi;
            :: else -> finalarray[i].aa[j] = 0;
            fi;
        fi;
        j = j+1;
        od;
        i=i+1;
      od;



    printf("Length of LCS: %d\n",result);



}

init {
        byte i,j,v,result;
        initArray1();
        initArray2();
        LCSsubstr();



}