Next: Bibliography
Up: Supervised Synthesis
Previous: Supervised Synthesis
Applying Heuristics
In this section, we show how developers of fault-tolerance can select suitable heuristics where they need to resolve deadlock states. The deadlock resolution step follows after the removal of safety-violating transitions.
In the main menu of the framework, there exists an option related to deadlock resolution (i.e., the option S). Upon selection of the option S, the following menu appears:
1: Heuristic1.
2: Heuristic2.
3: Return.
The above menu provides the choice of selecting one of the existing heuristics for deadlock resolution. Developers of fault-tolerance can select one of the existing heuristics during the synthesis. The number of existing heuristics depends on the heuristics that are currently integrated into the framework. We note that as developers design new heuristics, they can integrate them into the framework and add new options to the above menu in GraphImplementation2.java file. The integration of new heuristics is fairly simple. We refer the interested readers to [#!frmwrktech!#] for the details of integrating new heuristics to the framework..
APPENDIX
[commandchars=\\\{\},
numbers=left,numbersep=3pt, fontsize=\footnotesize,
xleftmargin=10mm,xrightmargin=10mm]
/* Copyright (C) 2002 Ali Ebnenasir.
*
* Do not modify without amending copyright; distribute freely but retain
* copyright message.
*
* Java files generated by running JavaCC on this file (or modified versions
* of this file) may be used in exactly the same manner as this file.
*
* Author: Ali Ebnenasir
* Date: 9/29/02
*
* This file contains a grammar for specifying the input file of the SYNFT.
* In the input file, the user should specify a fault-intolerant program,
* its invariant, its specification, initial states, and faults.
*
*/
TOKEN : /* RESERVED WORDS AND LITERALS */
< PROGRAM: "program" >
| < VAR: "var" >
| < DOMAIN: "domain" >
| < PROCESS: "process" >
| < BEGIN: "begin" >
| < END: "end" >
| < READ: "read" >
| < WRITE: "write" >
| < BOOLEAN: "boolean" >
| < INT: "int" >
| < FALSE: "false" >
| < TRUE: "true" >
| < FAULT: "fault" >
| < INVARIANT: "invariant" >
| < SPECIFICATION: "specification" >
| < SOURCE: "source" >
| < DESTINATION: "destination" >
| < RELATION: "relation" >
| < INIT: "init" >
| < STATE: "state" >
| < NOSOURCE: "noSource" >
| < NODESTINATION: "noDestination" >
| < NORELATION: "noRelation" >
TOKEN : /* LITERALS */
< INTEGER_LITERAL:
<DECIMAL_LITERAL>
| <HEX_LITERAL>
>
|
< #DECIMAL_LITERAL>
|
< #HEX_LITERAL>
TOKEN : /* SEPARATORS */
< LPAREN: "(" >
| < RPAREN: ")" >
| < SEMICOLON: ";" >
| < COMMA: "," >
| < DOT: "." >
| < DOUBLEDOT: ".." >
| < ARROW: "->" >
| < BAR: "|" >
TOKEN : /* OPERATORS */
< ASSIGN: "=" >
| < GT: ">" >
| < LT: "<" >
| < BANG: "!" >
| < EQ: "==" >
| < LE: "<=" >
| < GE: ">=" >
| < NE: "!=" >
| < AND: "&&" >
| < PLUS: "+" >
| < MINUS: "-" >
| < REM: "%" >
| < TILDA: "~" >
| < OR: "||" >
/***********************************************
* THE LANGUAGE GRAMMAR STARTS HERE *
***********************************************/
/*
* Program syntax follows.
*/
InputProgram() :
( ProgramDeclarator() )
( VariableDeclarator() )
( ProcessDeclarator() )+
(FaultDeclarator())
(Invariant())
(Specification())
(Initialization())
ProgramDeclarator() : "program" Name()
VariableDeclarator() : "var" VarDeclaration()
VarDeclaration() :
( BooleanDeclaration() | IntegerDeclaration())+
BooleanDeclaration() :
"boolean" VariableId() [ "=" Literal() ] ";"
IntegerDeclaration() :
"int" VariableId() [ "=" Literal()] ","
DomainDeclarator() ";"
VariableId() :
<IDENTIFIER> ( "[" "]" )*
DomainDeclarator() :
"domain" ( Literal() ".." Literal() )
( "~" Literal() ".." Literal() )*
Literal() :
<INTEGER_LITERAL>
|
BooleanLiteral()
BooleanLiteral() :
"true" | "false"
/*
* Process syntax follows.
*/
ProcessDeclarator() :
"process" Name()
"begin" ProcessBody() RWRestrictions() "end"
ProcessBody() :
Action() ("|" Action())*
/*
* Fault syntax follows.
*/
FaultDeclarator() :
"fault" Name()
"begin" FaultBody() "end"
FaultBody() :
Action() ("|" Action())*
/*
* Invariant syntax should be in DNF form.
*/
Invariant():
"invariant" BooleanExpression()
/*
* Specification syntax consists of two parts: source states and destination states.
*/
Specification():
"specification" ("destination" BooleanExpression() | "noDestination" )
("relation" BooleanExpression()
| "noRelation" )
/*
* Initialization syntax consists of variables value assignment.
*/
Initialization():
"init" ("state" ( InState() ) )*
InState():
( Statement() ";" )+
Action Action() :
BooleanExpression() "->"
( Statement() (t =";" | t=",") )+
RWRestrictions() :
"read" NameList() ";" "write" NameList() ";"
NameList() :
Name() ( "," Name() )*
Name() :
<IDENTIFIER>
Guard() :
( Conjunction()) ("||"Conjunction())*
term():
LOOKAHEAD(2) Comparison()
( LOOKAHEAD(2) ("&&" | "||")
Comparison() )* |
"(" BooleanExpression(expr) ")"
BooleanExpression() :
term() (LOOKAHEAD(2) ("&&" | "||") term() )*
Conjunction() :
"(" Comparison() ("&&" comp = Comparison() )*
")"
Disjunction() :
"(" Comparison() ("||" Comparison() )* ")"
Comparison():
"(" (( Literal() | Name() ) ComparisonOperators()
( Literal() | Name() ) ) ")"
ComparisonOperators() :
"==" | "!=" | "<" |
">" | "<=" | ">="
Statement() :
Name() "=" ( Literal() | Name() )
Ali Ebnenasir
2003-10-26