/******************************************************************************
 * Copyright (c) 2000-2014 Ericsson Telecom AB
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 ******************************************************************************/
module rotter_OK {

type component PDTestComponent {};


/*--- ROTATE ON BITSTRING --------------------------------------------------*/

const     bitstring rotconb := '1000110001'B // '0000000000'B
modulepar bitstring rotparb1 := rotconb
modulepar bitstring rotparb2 := rotconb @> 2 // '0110001100'B
modulepar bitstring rotparb3 := rotconb <@ 2 // '0011000110'B
modulepar bitstring rotparb4 := rotconb <@ 5 // '1000110001'B
modulepar bitstring rotparb5 := rotconb @> 5 // '1000110001'B
modulepar bitstring rotparb6 := rotconb <@ 0 // '1000110001'B
modulepar bitstring rotparb7 := rotconb @> 0 // '1000110001'B
modulepar bitstring rotparb8 := rotconb <@ 11 // '0001100011'B
modulepar bitstring rotparb9 := rotconb @> 11 // '1100011000'B
modulepar bitstring rotparb10 := ''B
modulepar bitstring rotparb11 := ''B @> 2
modulepar bitstring rotparb12 := ''B <@ 2
modulepar bitstring rotparb13 := ''B @> 0
modulepar bitstring rotparb14 := ''B <@ 0
modulepar bitstring rotparb15 := rotconb @> -2 // '0011000110'B
modulepar bitstring rotparb16 := rotconb <@ -2 // '0110001100'B

testcase rotate_bitstr() runs on PDTestComponent{

	var integer j;

	if (rotparb1 == rotparb1 <@ lengthof(rotparb1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb1 == rotparb1 @> lengthof(rotparb1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb1 == rotparb2 <@ 2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb1 == rotparb3 @> 2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb1 == rotparb4 @> 5)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb1 == rotparb5 <@ 5)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb1 == rotparb6)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb1 == rotparb7)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb8 == '0001100011'B)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb9 == '1100011000'B)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((rotparb10 == rotparb11)
	and (rotparb10 == rotparb12))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((rotparb10 == rotparb13)
	and (rotparb10 == rotparb14))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb15 == rotparb3)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparb16 == rotparb2)
	     {setverdict(pass);}
	else {setverdict(fail);}

	var bitstring b1 := '0000011111'B
	for (j:=0; j<15; j:=j+1) {
	if ((b1 <@ j) @> j == b1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((b1 <@ -j) <@ j == b1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((b1 @> -j) @> j == b1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((b1 @> 0 == b1)
	and (b1 <@ 0 == b1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	}

	var bitstring b2 := '10101010101010101010'B
	for (j:=1; j<30; j:=j+2) {
	if ((b2 <@ j) != b2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((b2 <@ j-1) == b2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((b2 @> j) != b2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((b2 @> j-1) == b2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	}


}

/*--- ROTATE ON HEXSTRING --------------------------------------------------*/

const     hexstring rotconh := '1000110001'H // '0000000000'H
modulepar hexstring rotparh1 := rotconh
modulepar hexstring rotparh2 := rotconh @> 2 // '0110001100'H
modulepar hexstring rotparh3 := rotconh <@ 2 // '0011000110'H
modulepar hexstring rotparh4 := rotconh <@ 5 // '1000110001'H
modulepar hexstring rotparh5 := rotconh @> 5 // '1000110001'H
modulepar hexstring rotparh6 := rotconh <@ 0 // '1000110001'H
modulepar hexstring rotparh7 := rotconh @> 0 // '1000110001'H
modulepar hexstring rotparh8 := rotconh <@ 11 // '0001100011'H
modulepar hexstring rotparh9 := rotconh @> 11 // '1100011000'H
modulepar hexstring rotparh10 := ''H
modulepar hexstring rotparh11 := ''H @> 2
modulepar hexstring rotparh12 := ''H <@ 2
modulepar hexstring rotparh13 := ''H @> 0
modulepar hexstring rotparh14 := ''H <@ 0
modulepar hexstring rotparh15 := rotconh @> -2 // '0011000110'H
modulepar hexstring rotparh16 := rotconh <@ -2 // '0110001100'H

testcase rotate_hexstr() runs on PDTestComponent{

	var integer j;


	if (rotparh1 == rotparh1 <@ lengthof(rotparh1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh1 == rotparh1 @> lengthof(rotparh1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh1 == rotparh2 <@ 2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh1 == rotparh3 @> 2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh1 == rotparh4 @> 5)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh1 == rotparh5 <@ 5)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh1 == rotparh6)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh1 == rotparh7)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh8 == '0001100011'H)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh9 == '1100011000'H)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((rotparh10 == rotparh11)
	and (rotparh10 == rotparh12))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((rotparh10 == rotparh13)
	and (rotparh10 == rotparh14))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh15 == rotparh3)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparh16 == rotparh2)
	     {setverdict(pass);}
	else {setverdict(fail);}

	var hexstring h1 := '0000011111'H
	for (j:=0; j<15; j:=j+1) {
	if ((h1 <@ j) @> j == h1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((h1 <@ -j) <@ j == h1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((h1 @> -j) @> j == h1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((h1 @> 0 == h1)
	and (h1 <@ 0 == h1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	}

	var hexstring h2 := '10101010101010101010'H
	for (j:=1; j<30; j:=j+2) {
	if ((h2 <@ j) != h2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((h2 <@ j-1) == h2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((h2 @> j) != h2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((h2 @> j-1) == h2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	}


}

/*--- ROTATE ON OCTETSTRING --------------------------------------------------*/

const octetstring rotcono  := 'AA00AA00AA'O
modulepar octetstring rotparo1 := rotcono
modulepar octetstring rotparo2 := rotcono @> 1 // 'AAAA00AA00'O
modulepar octetstring rotparo3 := rotcono <@ 1 // '00AA00AAAA'O
modulepar octetstring rotparo4 := rotcono <@ 5 // 'AA00AA00AA'O
modulepar octetstring rotparo5 := rotcono @> 5 // 'AA00AA00AA'O
modulepar octetstring rotparo6 := rotcono <@ 0 // 'AA00AA00AA'O
modulepar octetstring rotparo7 := rotcono @> 0 // 'AA00AA00AA'O
modulepar octetstring rotparo8 := rotcono <@ 11 // '00AA00AAAA'O
modulepar octetstring rotparo9 := rotcono @> 11 // 'AAAA00AA00'O
modulepar octetstring rotparo10 := ''O
modulepar octetstring rotparo11 := ''O @> 2
modulepar octetstring rotparo12 := ''O <@ 2
modulepar octetstring rotparo13 := ''O @> 0
modulepar octetstring rotparo14 := ''O <@ 0
modulepar octetstring rotparo15 := rotcono @> -1 // '00AA00AAAA'O
modulepar octetstring rotparo16 := rotcono <@ -1 // 'AAAA00AA00'O

testcase rotate_octetstr() runs on PDTestComponent{

	var integer j;

	if (rotparo1 == rotparo1 <@ lengthof(rotparo1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo1 == rotparo1 @> lengthof(rotparo1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo1 == rotparo2 <@ 1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo1 == rotparo3 @> 1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo1 == rotparo4 @> 5)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo1 == rotparo5 <@ 5)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo1 == rotparo6)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo1 == rotparo7)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo8 == '00AA00AAAA'O)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo9 == 'AAAA00AA00'O)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((rotparo10 == rotparo11)
	and (rotparo10 == rotparo12))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((rotparo10 == rotparo13)
	and (rotparo10 == rotparo14))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo15 == rotparo3)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparo16 == rotparo2)
	     {setverdict(pass);}
	else {setverdict(fail);}


	var octetstring o1 := '0000011111'O
	for (j:=0; j<15; j:=j+1) {
	if ((o1 <@ j) @> j == o1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((o1 <@ -j) <@ j == o1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((o1 @> -j) @> j == o1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((o1 @> 0 == o1)
	and (o1 <@ 0 == o1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	}

	var octetstring o2 := '1100110011001100110011001100110011001100'O
	for (j:=1; j<30; j:=j+2) {
	if ((o2 <@ j) != o2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((o2 <@ j-1) == o2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((o2 @> j) != o2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((o2 @> j-1) == o2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	}

}

/*--- ROTATE ON CHARSTRING --------------------------------------------------*/

const     charstring rotconc := "1000110001" // "0000000000"
modulepar charstring rotparc1 := rotconc
modulepar charstring rotparc2 := rotconc @> 2 // "0110001100"
modulepar charstring rotparc3 := rotconc <@ 2 // "0011000110"
modulepar charstring rotparc4 := rotconc <@ 5 // "1000110001"
modulepar charstring rotparc5 := rotconc @> 5 // "1000110001"
modulepar charstring rotparc6 := rotconc <@ 0 // "1000110001"
modulepar charstring rotparc7 := rotconc @> 0 // "1000110001"
modulepar charstring rotparc8 := rotconc <@ 11 // "0001100011"
modulepar charstring rotparc9 := rotconc @> 11 // "1100011000"
modulepar charstring rotparc10 := ""
modulepar charstring rotparc11 := "" @> 2
modulepar charstring rotparc12 := "" <@ 2
modulepar charstring rotparc13 := "" @> 0
modulepar charstring rotparc14 := "" <@ 0
modulepar charstring rotparc15 := rotconc @> -2 // "0011000110"
modulepar charstring rotparc16 := rotconc <@ -2 // "0110001100"

testcase rotate_char() runs on PDTestComponent{

	var integer j;

	if (rotparc1 == rotparc1 <@ lengthof(rotparc1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc1 == rotparc1 @> lengthof(rotparc1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc1 == rotparc2 <@ 2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc1 == rotparc3 @> 2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc1 == rotparc4 @> 5)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc1 == rotparc5 <@ 5)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc1 == rotparc6)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc1 == rotparc7)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc8 == "0001100011")
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc9 == "1100011000")
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((rotparc10 == rotparc11)
	and (rotparc10 == rotparc12))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((rotparc10 == rotparc13)
	and (rotparc10 == rotparc14))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc15 == rotparc3)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparc16 == rotparc2)
	     {setverdict(pass);}
	else {setverdict(fail);}

	var charstring c1 := "0000011111"
	for (j:=0; j<15; j:=j+1) {

	if ((c1 <@ j) @> j == c1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c1 <@ -j) <@ j == c1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c1 @> -j) @> j == c1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c1 @> 0 == c1)
	and (c1 <@ 0 == c1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	}

	var charstring c2 := "10101010101010101010"
	for (j:=1; j<30; j:=j+2) {
	if ((c2 <@ j) != c2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c2 <@ j-1) == c2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c2 @> j) != c2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c2 @> j-1) == c2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	}


}


/*--- ROTATE ON UNIVERSAL CHARSTRING --------------------------------------------------*/

//modulepar universal charstring rotconuc := "0000000000"
const     universal charstring rotconuc  := char(0,0,0,65) & "000" & char(0,0,0,65) & char(0,0,0,65) & "000" & char(0,0,0,65) //A000AA000A
modulepar universal charstring rotparuc1 := rotconuc
modulepar universal charstring rotparuc2 := rotconuc @> 2 		// "0AA000AA00"
modulepar universal charstring rotparuc3 := rotconuc <@ 2 		// "00AA000AA0"
modulepar universal charstring rotparuc4 := rotconuc <@ 5 		// "A000AA000A"
modulepar universal charstring rotparuc5 := rotconuc @> 5 		// "A000AA000A"
modulepar universal charstring rotparuc6 := rotconuc <@ 0 		// "A000AA000A"
modulepar universal charstring rotparuc7 := rotconuc @> 0 		// "A000AA000A"
modulepar universal charstring rotparuc8 := rotconuc <@ 11 	// "000AA000AA"
modulepar universal charstring rotparuc9 := rotconuc @> 11 	// "AA000AA000"
modulepar universal charstring rotparuc10 := ""
modulepar universal charstring rotparuc11 := "" @> 2
modulepar universal charstring rotparuc12 := "" <@ 2
modulepar universal charstring rotparuc13 := "" @> 0
modulepar universal charstring rotparuc14 := "" <@ 0
modulepar universal charstring rotparuc15 := rotconuc @> -2 	// "00AA000AA0"
modulepar universal charstring rotparuc16 := rotconuc <@ -2 	// "0AA000AA00"

testcase rotate_uchar() runs on PDTestComponent{

	var integer j;
	if (rotparuc1 == rotparuc1 <@ lengthof(rotparc1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc1 == rotparuc1 @> lengthof(rotparc1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc1 == rotparuc2 <@ 2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc1 == rotparuc3 @> 2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc1 == rotparuc4 @> 5)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc1 == rotparuc5 <@ 5)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc1 == rotparuc6)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc1 == rotparuc7)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc8 == "000AA000AA")
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc9 == "AA000AA000")
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((rotparuc10 == rotparuc11)
	and (rotparuc10 == rotparuc12))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((rotparuc10 == rotparuc13)
	and (rotparuc10 == rotparuc14))
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc15 == rotparuc3)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if (rotparuc16 == rotparuc2)
	     {setverdict(pass);}
	else {setverdict(fail);}

	var universal charstring c1 := "0000011111"
	for (j:=0; j<15; j:=j+1) {

	if ((c1 <@ j) @> j == c1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c1 <@ -j) <@ j == c1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c1 @> -j) @> j == c1)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c1 @> 0 == c1)
	and (c1 <@ 0 == c1))
	     {setverdict(pass);}
	else {setverdict(fail);}
	}

	var charstring c2 := "10101010101010101010"
	for (j:=1; j<30; j:=j+2) {
	if ((c2 <@ j) != c2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c2 <@ j-1) == c2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c2 @> j) != c2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	if ((c2 @> j-1) == c2)
	     {setverdict(pass);}
	else {setverdict(fail);}
	}
}

control {
	execute (rotate_bitstr());
	execute (rotate_hexstr());
	execute (rotate_octetstr());
	execute (rotate_char());
	execute (rotate_uchar());
}

}