/*
 The test is taken from the paper:
 M.T Trinh, D.H Chu, J. Jaffar, Progressive reasoning over recursively-defined strings /
 International Conference on Computer Aided Verification, 218-240

 The program checks the consistency of the following sanitization procedure.
 Given a string, we replace all the symbols '<' to the tag '&lt', and all the '>' to the tag '&rt'.
 We say the sanitization is correct if the resulting string does not contain '<script'.

 The functions ReplaceBr1 and ReplaceBr2 model the sanitization. The function Check checks if it is correct.
 The resulting program does not contain functions returning 'F', 
 hence the sanitization is proven to be correct in respect to the given condition.

*/

/***********************************************/
/*           the input program                 */
/***********************************************/

$ENTRY Go {
   e.p = <Check <ReplaceBr1 e.p>>;
}

ReplaceBr1 {
    e.x1 '<' e.x2 = <ReplaceBr2 e.x1'&lt'><ReplaceBr1 e.x2>;
    e.Other = <ReplaceBr2 e.Other>;
}

ReplaceBr2 {
    e.x1 '>' e.x2 =  e.x1'&rt'<ReplaceBr2 e.x2>;
    e.Other = e.Other;
}


Check {
    = 'T';
    '<script'e.x2 = 'F';
    t.y1 e.Z = <Check e.Z>;
}


/***********************************************/
/*          the residual program               */
/***********************************************/

/*
$ENTRY Go {
 e.x1 =  <Check_1 e.x1>;
}


Check_1 {
 e.x1 '<' e.x2 =  <Check_0 (e.x1) (e.x2)>;
 e.x1 =  <Check_2 e.x1>;
}


Check_3_0 {
 (t.y1 e.x1) (e.x2) (e.x3) =  <Check_3_0 (e.x1) (e.x2) (e.x3)>;
 () (e.x1) (e.x2) =  <Check_0 (e.x1) (e.x2)>;
}


Check_0 {
 (e.x1 '>' e.x2) (e.x3) =  <Check_3_0 (e.x1) (e.x2) (e.x3)>;
 (e.x1) (e.x2) =  <Check_3_1 (e.x1) (e.x2)>;
}


Check_3_1 {
 (t.y1 e.x1) (e.x2) =  <Check_3_1 (e.x1) (e.x2)>;
 () (e.x1) =  <Check_1 e.x1>;
}


Check_3_2 {
 (t.y1 e.x1) (e.x2) =  <Check_3_2 (e.x1) (e.x2)>;
 () (e.x1) =  <Check_2 e.x1>;
}


Check_2 {
 e.x1 '>' e.x2 =  <Check_3_2 (e.x1) (e.x2)>;
 e.x1 =  <Check_13_0 e.x1>;
}


Check_13_0 {
 =  'T';
 t.y1 e.x1 =  <Check_13_0 e.x1>;
}

*/