/******************************************************************************
* Copyright (c) 2000-2021 Ericsson Telecom AB
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v2.0
* which accompanies this distribution, and is available at
* https://www.eclipse.org/org/documents/epl-2.0/EPL-2.0.html
*
* Contributors:
*   Balasko, Jeno
*   Baranyi, Botond
*   Kovacs, Ferenc
*   Raduly, Csaba
*   Szabados, Kristof
*   Szabo, Janos Zoltan – initial implementation
*
******************************************************************************/
module TboolOper
{

modulepar boolean tsp_uninit;
modulepar boolean tsp_init := true;

const boolean TboolOper_const1:=true;
type component boolOper_comptype { };

testcase boolAssign() runs on boolOper_comptype
{ var boolean x1:=true;
  var boolean x4:=x1;
  var boolean x2,x3;
  x2:=false;
  x3:=x2;
  if (x1) {setverdict(pass);}	//at declaration, value
  else {setverdict(fail);}
  if (x4) {setverdict(pass);}	//at declaration, variable
  else {setverdict(fail);}
  if (not(x2)) {setverdict(pass);}	//later, value
  else {setverdict(fail);}
  if (not(x3)) {setverdict(pass);}	//later, variable
  else {setverdict(fail);}
}

testcase boolConst() runs on boolOper_comptype {
  const boolean TboolOper_const3:=false;
  if (TboolOper_const1) {setverdict(pass);}	//definition part
  else {setverdict(fail);}
  //if (TboolOper_const2==2) {setverdict(pass);}	//control part
  //     else {setverdict(fail);}
  if (not(TboolOper_const3)) {setverdict(pass);}	//testcase
  else {setverdict(fail);}
}

testcase boolCompEq() runs on boolOper_comptype
{ var boolean x1,x2,x3;
  x1:=true;
  x2:=true;
  x3:=false;
  if (x1==x2) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (not(x3==x2)) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (x1==true) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (not(x1==false)) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (true==x1) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (not(false==x1)) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (true==true) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
  if (not(true==false)) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
}

testcase boolCompNotEq() runs on boolOper_comptype
{ var boolean x1,x2,x3;
  x1:=true;
  x2:=false;
  x3:=true;
  if (x1!=x2) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (not(x1!=x3)) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (x1!=false) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (not(x1!=true)) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (true!=x2) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (not(false!=x2)) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (true!=false) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
  if (not(false!=false)) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
}

testcase boolNot() runs on boolOper_comptype
{ var boolean x1,x2,x3,x4,x5,x6;
  x1:=true;
  x2:=false;
  x3:=not(x1);
  x4:=not(x2);
  x5:=not(true);
  x6:=not(false);
  if (not(x3)) {setverdict(pass);}	//variable
  else {setverdict(fail);}
  if (x4) {setverdict(pass);}		//variable
  else {setverdict(fail);}
  if (not(x5)) {setverdict(pass);}	//value
  else {setverdict(fail);}
  if (x6) {setverdict(pass);}		//value
  else {setverdict(fail);}
}

testcase boolAnd() runs on boolOper_comptype
{ var boolean x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18;
  x1:=true;
  x2:=false;
  x3:=x1 and x1;
  x4:=x1 and x2;
  x5:=x2 and x1;
  x6:=x2 and x2;
  x7:=x1 and true;
  x8:=x1 and false;
  x9:=x2 and true;
  x10:=x2 and false;
  x11:=true and x1;
  x12:=true and x2;
  x13:=false and x1;
  x14:=false and x2;
  x15:=true and true;
  x16:=true and false;
  x17:=false and true;
  x18:=false and false;
  if (x3) {setverdict(pass);}		//variable_variable
  else {setverdict(fail);}
  if (not(x4)) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (not(x5)) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (not(x6)) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (x7) {setverdict(pass);}		//variable_value
  else {setverdict(fail);}
  if (not(x8)) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (not(x9)) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (not(x10)) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (x11) {setverdict(pass);}		//value_variable
  else {setverdict(fail);}
  if (not(x12)) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (not(x13)) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (not(x14)) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (x15) {setverdict(pass);}		//value_value
  else {setverdict(fail);}
  if (not(x16)) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
  if (not(x17)) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
  if (not(x18)) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
}

testcase boolOr() runs on boolOper_comptype
{ var boolean x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18;
  x1:=true;
  x2:=false;
  x3:=x1 or x1;
  x4:=x1 or x2;
  x5:=x2 or x1;
  x6:=x2 or x2;
  x7:=x1 or true;
  x8:=x1 or false;
  x9:=x2 or true;
  x10:=x2 or false;
  x11:=true or x1;
  x12:=true or x2;
  x13:=false or x1;
  x14:=false or x2;
  x15:=true or true;
  x16:=true or false;
  x17:=false or true;
  x18:=false or false;
  if (x3) {setverdict(pass);}		//variable_variable
  else {setverdict(fail);}
  if (x4) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (x5) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (not(x6)) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (x7) {setverdict(pass);}		//variable_value
  else {setverdict(fail);}
  if (x8) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (x9) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (not(x10)) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (x11) {setverdict(pass);}		//value_variable
  else {setverdict(fail);}
  if (x12) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (x13) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (not(x14)) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (x15) {setverdict(pass);}		//value_value
  else {setverdict(fail);}
  if (x16) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
  if (x17) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
  if (not(x18)) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
}

testcase boolXor() runs on boolOper_comptype
{ var boolean x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18;
  x1:=true;
  x2:=false;
  x3:=x1 xor x1;
  x4:=x1 xor x2;
  x5:=x2 xor x1;
  x6:=x2 xor x2;
  x7:=x1 xor true;
  x8:=x1 xor false;
  x9:=x2 xor true;
  x10:=x2 xor false;
  x11:=true xor x1;
  x12:=true xor x2;
  x13:=false xor x1;
  x14:=false xor x2;
  x15:=true xor true;
  x16:=true xor false;
  x17:=false xor true;
  x18:=false xor false;
  if (not(x3)) {setverdict(pass);}		//variable_variable
  else {setverdict(fail);}
  if (x4) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (x5) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (not(x6)) {setverdict(pass);}	//variable_variable
  else {setverdict(fail);}
  if (not(x7)) {setverdict(pass);}		//variable_value
  else {setverdict(fail);}
  if (x8) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (x9) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (not(x10)) {setverdict(pass);}	//variable_value
  else {setverdict(fail);}
  if (not(x11)) {setverdict(pass);}		//value_variable
  else {setverdict(fail);}
  if (x12) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (x13) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (not(x14)) {setverdict(pass);}	//value_variable
  else {setverdict(fail);}
  if (not(x15)) {setverdict(pass);}		//value_value
  else {setverdict(fail);}
  if (x16) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
  if (x17) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
  if (not(x18)) {setverdict(pass);}	//value_value
  else {setverdict(fail);}
}

testcase boolUninitXor() runs on boolOper_comptype {
  var boolean x1,x2,x3;
  x1:=true;
  @try {
    x3:=x1 xor x2;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x3:=x2 xor x1;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x3:= true xor x2;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x3:=x2 xor true;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
}

testcase boolUninitOr() runs on boolOper_comptype {
  var boolean x1,x2,x3;
  x1:=false; 
  @try {
    x3:=x1 or x2;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x3:=x2 or x1;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x3:= false or x2;
    if(x3 != true) {setverdict(fail, "true or DTE expected")}
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x3:=x2 or true;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
}

testcase boolUninitAnd() runs on boolOper_comptype {
  var boolean x1,x2,x3;
  x1:=true;
  @try {
    x3:=x1 and x2;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x3:=x2 and x1;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x3:= true and x2;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x3:=x2 and true;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
}

testcase boolUninitNot() runs on boolOper_comptype {
  var boolean x1,x2;
  @try {
    x2:= not x1;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
}

testcase boolUninitLog() runs on boolOper_comptype {
  var boolean x1;
  if (log2str(x1) == "<unbound>") { 
    setverdict(pass, "x1: ",x1);
  } else { 
    setverdict(fail);
  }
}

testcase boolUninitTemplate() runs on boolOper_comptype {
  var template boolean x2;
  var boolean x1;
  @try {
    x2:= x1;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x2:= not x1;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }

  @try {
    x1:= valueof(x2);
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
}

testcase boolModulepar() runs on boolOper_comptype {
  var template boolean x2;
  var boolean x1 := true;
  @try {
    x2:= tsp_uninit;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  @try {
    x2:= not tsp_uninit;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }

  @try {
    x2:= tsp_uninit or x1;
    setverdict(fail, "This line should not be reached. DTE expected")
  } @catch(e) {
    //check e
    setverdict(pass);
  }
  if (true != tsp_init) { 
    setverdict(fail);
  }
  if (log2str(tsp_uninit) == "<unbound>") { 
    setverdict(pass);
  } else { 
    setverdict(fail);
  }
  if (log2str(tsp_init) != "true") {
    setverdict(fail);
  }
}

type boolean myb1
type boolean myb2 (true)
type boolean myb3 (false)
// FATAL_ERROR() with R8B: `type boolean myb3 (true, valueof(t_myb1));'
type boolean myb4 (c_myb1, not c_myb1 and c_myb1);
type myb3 myb5
type boolean myb6 (myb2, myb3)

const boolean c_myb1 := true
const myb6 c_myb2 := c_myb1

template boolean t_myb1 := true
template myb6 t_myb2 := t_myb1

function f_b1(in boolean p1) return boolean { return p1 }

function f_b2() return myb4 {
  var template boolean vt_myb1 := t_myb1
  if (valueof(t_myb1) and valueof(vt_myb1)) { return true }
  else { return false }
}

function f_b3() return myb4 {
  var myb4 v_myb1 := false
  var template myb4 vt_myb1 := c_myb1
  if (not v_myb1 and valueof(vt_myb1) == true) { return true }
  else { return false }
}

testcase boolSubtypes() runs on boolOper_comptype {
  if (f_b1(c_myb1) == f_b2()) { setverdict(pass) }
  else { setverdict(fail) }
}

testcase boolIsvalue() runs on boolOper_comptype{
  var template boolean vt0;
  var template boolean vt1 := ( true, true, true );

  if ( isvalue(vt0) ) { setverdict(fail); } else { setverdict(pass); };
  if ( isvalue(vt1) ) { setverdict(fail); } else { setverdict(pass); };

  var boolean x1 := true;
  if (isvalue(x1) ){ 
    setverdict (pass);
  } else  {
    setverdict (fail);
  }
}

type union TestUnion {
  integer t,
  boolean b
}

type record TestRecord {
  integer t,
  boolean b optional
}

// for TR fix HT60781
testcase boolShortCircuit() runs on boolOper_comptype {
  // create a union variable, make sure the boolean field is not chosen
  var TestUnion myUnion := { t := 1 };

  // reference the boolean field in the 2nd part of a condition using 'and' or 'or'
  // only the first part of the condition should be evaluated, since
  // evaluating the 2nd part would produce a DTE (because the field isn't chosen)
  if (ischosen(myUnion.b) and myUnion.b) {
    setverdict(fail, "Error in 'if' condition, field 'b' is not supposed to be chosen");
  }
  while (ischosen(myUnion.b) and myUnion.b) {
    setverdict(fail, "Error in 'while' condition, field 'b' is not supposed to be chosen");
  }
  var integer i;
  for (i := 0; ischosen(myUnion.b) and myUnion.b and i < 5; i := i + 1) {
    setverdict(fail, "Error in 'for' condition, field 'b' is not supposed to be chosen");
  }
  var boolean res := not ischosen(myUnion.b) or myUnion.b;
  if (not res) {
    setverdict(fail, "Error in boolean assignment, field 'b' is not supposed to be chosen");
  }

  // create a record variable, make sure the boolean field is omitted
  var TestRecord myRec := { t := 1, b := omit };

  // reference the boolean field in the 2nd part of a condition, same as with the union field
  // (referencing the boolean field would cause a DTE again, because it is omitted)
  if (ispresent(myRec.b) and myRec.b) {
    setverdict(fail, "Error in 'if' condition, field 'b' is not supposed to be present");
  }
  while (ispresent(myRec.b) and myRec.b) {
    setverdict(fail, "Error in 'if' condition, field 'b' is not supposed to be present");
  }
  for (i := 0; ispresent(myRec.b) and myRec.b and i < 5; i := i + 1) {
    setverdict(fail, "Error in 'for' condition, field 'b' is not supposed to be present");
  }
  res := not ispresent(myRec.b) or myRec.b;
  if (not res) {
    setverdict(fail, "Error in boolean assignment, field 'b' is not supposed to be present");
  }
  setverdict(pass);
}

testcase boolUnion() runs on boolOper_comptype {
  // create a union variable, make sure the boolean field is not chosen
  var TestUnion myUnion := { b := true };
  if (ischosen(myUnion.b))  {
    setverdict(pass,"The value of the field: ", myUnion.b);
  }

}

type record MyRecord {
  integer a optional
}

// comparing an optional record field to 'omit' in a boolean variable assignment (bug 498430)
testcase boolCompEqOmit() runs on boolOper_comptype {
  var MyRecord myRecord := { a := omit };
  var boolean b := myRecord.a == omit;
  if (b == true) { setverdict(pass); }
  else { setverdict(fail); }
}

control {
  const boolean cl_1:=true;
  var boolean vl_1;

  execute(boolAssign());
  execute(boolConst());
  execute(boolCompEq());
  execute(boolCompNotEq());
  execute(boolNot());
  execute(boolAnd());
  execute(boolOr());
  execute(boolXor());
  execute(boolSubtypes());
  execute(boolIsvalue());
  execute(boolShortCircuit());
  execute(boolCompEqOmit());
  execute(boolUninitXor());
  execute(boolUninitOr());
  execute(boolUninitAnd());
  execute(boolUninitNot());
  execute(boolUninitLog());
  execute(boolUninitTemplate());
  execute(boolModulepar());
  execute(boolUnion());
}

}