# ***************************************************************************
# * FC2 PACKAGE SOURCE FILE
# * 
# * help-sections.tcl -- Tcl Help Sections
# ***************************************************************************
section "What is Xeve?" {
    mark "What is Xeve?"
    bf "Xeve "
    rm "is a graphical interface environment for the (symbolic) analysis "
    rm "and verification of Esterel programs modeled as "
    bf "Finite State Machines (FSM)."
    cr
    par "Its main features are: "
    enumerate {
        item {
            ref "FSM model construction, " "The Verification Techniques"\
                    "The Verification Techniques"
        }
        item {
            ref "Output emission status checking "\
                    "Observers and Output Emission Checking"\
                    "Observers and Output Emission Checking"
            rm "used as a back-end of model-checking of safety properties "
            rm "expressed by observers. Diagnostic paths generated from "
            rm "model-checking are loadable in the tape reader of the "
            rm "Esterel graphical simulator Xes."
        }
        item {
            ref "FSM minimization "\
                    "FSM Reduction and Visualization" \
                    "FSM Reduction and Visualization"
            rm "with respect to the bisimulation "
	    rm "equivalence. The minimized FSM is saved in a textual "
            rm "format called fc2. One can explore graphically an FSM "
	    rm "described in fc2 using the Autograph tool. Autograph can be "
	    rm "downloded from "
            rm "http://www.inria.fr/meije/verification/downloads.html."
        }
    }
    par "Xeve's GUI is implemented in Tcl/Tk. FSMs are represented symbolically "
    rm "with BDDs using the TiGeR system data structures and libraries "
    rm "(see "
    ref "credits" "Credits" "Credits"
    rm "). The verification algorithms work on the BDD representation."
    cr
    rm " Xeve is developed jointly by INRIA and Ecole des "
    rm "Mines/CMA as part of the MEIJE research team." 
    cr
    par "More informations can be obtained visiting the WEB site "
    tt "http://www.esterel.org/ "
    rm "or by contacting the esterel team ("
    tt "esterel-request@sophia.inria.fr"
    rm ")."
}

section "On-line Help Features" {
    mark "On-line Help Features"
    bf "Xeve"
    rm " provides three ways of getting help:"
    enumerate {
        item {
            bf "This help (see "
            ref "credits" "Credits" "Credits"
            rm ")."
        }
        item {
            bf "A help for beginners: "
            rm "This help is enabled when the checkbutton "
            rm "\"Beginner's Mode\" "
            rm "on top of the main panel is set on. A help text is displayed "
            rm "on a message window at each main function calls. "
            rm "The information window is automatically dismissed at each "
            rm "new function call. The user can also dismiss it manually. "
            rm "By default, this help is set off."
        }
        item {
            bf "Balloon help: "
            rm "A balloon help appears on the main buttons and areas of the "
            rm "interface. It appears a little time after the cursor has "
            rm "entered and moved "
            rm "inside a button or an area where a balloon help is defined. "
            rm "The balloon help is displayed off when the cursor leaves the "
            rm "button or the area, or if you type any key on the keyboard. "
            rm "By default, the balloon help is activated. To set them off, "
            rm "pull down the help menu \"Options\" and toggle off the "
            rm "\"Balloon Help\" checkbutton, (see "
            ref "credits" "Credits" "Credits"
            rm ")."
        }
    }
}

section "Inputting an FSM" {
    mark "Inputting an FSM"
    rm "An FSM can be loaded from two types of file: "
    enumerate {
        item {
            bf "Blif file: "
            rm "This is the "
            it "Berkeley Logical Interchange Format"
            rm " to describe a set of boolean equations with latches, "
            rm "defining an implicit FSM. Using the Esterel compiler one can "
            rm "compile any Esterel program into a set of boolean equations "
            rm "with latches. The compiler can generate the equations in the "
            rm "Blif format. Blif is useful as it is accepted by a lot of "
            rm "synthesis and verification tools such as TiGeR. "
            rm "Xeve uses TiGeR to represent FSMs and to build and manipulate "
            rm "them symbolically using BDDs from their Blif description."
        }
        item {
            bf "Bddf file: "
            rm "BDDs are a powerful way to manipulate very large FSMs "
            rm "efficiently. However, BDD construction may take time, "
            rm "particularly the BDD of the reachable state space of the "
            rm "FSM. The TiGeR library provides an ASCII format called Bddf "
            rm "to save the FSM BDDs in this format, once they have "
            rm "been computed. You can save any FSM in this format using the "
            rm "menu entry \"Files:Save FSM\" and load any "
            rm "saved Bddf file. This avoids the re-computation of the FSM "
            rm "BDDs and reachable state space."
        }
    }
    par "To load a "
    bf "Blif"
    rm " file, use the entry menu \"Files:Open Blif file\". "
    rm "A file selection box browser appears for file selection. "
    par "After a file selection, a Yes/No window is displayed asking you "
    rm "if you need to load some input constraints over the inputs of the "
    rm "program. These constrains must be also described in a Blif file as "
    rm "a combinational circuit over the inputs. These constraints are "
    rm "the input relations you may have defined on your Esterel "
    rm "program. If so, answer Yes to select a relation file."
    cr
    par "To load a "
    bf "Bddf"
    rm " file, use the entry menu \"Files:Open Bddf file\". "
    rm "In this case, no relation file is asked (it is supposed to be "
    rm "already computed in)."
    cr
    par "The selected file names "
    rm "are reported in the main panel. Selection "
    rm "can still be made by hand by directly typing in the entry spaces "
    rm "where the files names are put. The <Return> key validates the choice."
    par "At opening time, the described symbolic FSM is "
    rm "internally built and its input/output interface is displayed on the "
    rm "main panel. If a bad file is given, an error message window is "
    rm "popped-up."
}

section "The Verification Techniques" {
    mark "The Verification Techniques"
    bf "Xeve"
    rm " performs some verification on the FSM model. It requires the "
    rm "reachable state set of the FSM under analysis. So any verification "
    rm "starts first by the computation of this set. This set is effectively "
    rm "computed if it has not been computed before so that it is computed "
    rm "only once in a session of a given FSM."
    cr
    par
    bf "Xeve"
    rm " provides two verification functions: "
    enumerate {
        item {
            rm "The "
            ref "minimization " "FSM Reduction and Visualization" "FSM Reduction and Visualization"
            rm "of the number of states of a FSM with respect to an "
            rm "equivalence called "
            it "bisimulation. "
            rm "The minimization is made modulo input and output signal "
            ref "hiding, "\
                    "Hiding, Observing or Fixing Signals"\
                    "Hiding, Observing or Fixing Signals"

        }
        item {
            rm "The other is the "
            ref "checking of the emission" "Observers and Output Emission Checking" "Observers and Output Emission Checking"
            rm " status of output signals. The checking is made on the "
            rm "selected output signals and modulo fixed or hidden input "
            rm "signals." 
            
        }
    }
}

section "Hiding, Observing or Fixing Signals" {
    mark "Hiding, Observing or Fixing Signals"
    rm "You can modulate the verification by selecting the signals that "
    rm "are relevant for you. You may hide signals from observation, or fix "
    rm "some of them to a constant value (0 for absent or 1 for present)."
    rm "Different possibilities are offered depending "
    rm "on the verification function that is under selection. A particular "
    rm "palette of colors is provided for each, with a particular meaning "
    rm "of the colors in each case. Two modes are provided in order to "
    rm "set a signal to some color. Though it has a particular meaning in "
    rm "each case, the signal fixing mechanism is the same in both case."

    subsection "Signal fixing mechanism" {
        rm "There are two modes for fixing signals: the "
        bf "selection mode "
        rm "and the "
        bf "painting mode."
        cr ; cr
        bf "Selection mode: "
        rm "A signal list area is in selection mode whenever the button "
        rm "on the bottom of the signal list area that represents a "
        rm "selection arrow is in a sunken"
        rm "relief. The selection mode allows you to select signals with "
        rm "mouse clicks possibly in conjunction with keyboard keys "
        rm "(see next section). A selected "
        rm "signal appears with a gray background. To fix the selected "
        rm "signals to a specific color, just  click on the desired color. "
        rm "After such a coloring, the selection remains in its state."
        cr ; cr
        bf "Painting mode: "
        rm "A signal list area is in painting mode whenever the"
        rm "button on the bottom of the signal list area that represents a"
        rm "painting brush is in a sunken relief. To pain signals in some "
        rm "color, select that color. Then pass over the signals with "
        rm "mouse clicks possibly in conjunction with keyboard keys "
        rm "(see next section), to color them in the selected color."
    }
    subsection "Mouse/Keyboard events for signal fixing" {
        mark "Mouse/Keyboard events for signal fixing"
        rm "The mouse clicks and keyboard keys to select or paint signals are:"
        cr
        itemize {
            item {
                bf "<Control-a> | <Control-A>: "
                rm "global selection/painting"
            }
            item {
                bf "<Button-1>: "
                rm "select/paint the underlying signal. In selection mode "
                rm "deselects all other selected signals."
            }
            item {
                bf "<Button-1-Motion>:"
                itemize {
                    item {
                        rm "selection mode: select all the signals from the "
                        rm "firstly selected signal to the lastly selected "
                        rm "one."
                    }
                    item {
                        rm "painting mode: paint all the signals on "
                        rm "which the brush passes over."
                    }
                }
            }
            item {
                bf " <Shift-Button-1>:"
                itemize {
                    item {
                        rm "selection mode: select all the signals from the "
                        rm "lastly selected signal to the underlying signal."
                    }
                    item {
                        rm "painting mode : same as <Button-1>."
                    }
                }
            }
            item {
                bf "<Control-Button-1>:"
                itemize {
                    item {
                        rm "selection mode: add to the current selection "
                        rm "the underlying signal."
                    }
                    item {
                        rm "painting mode : same as <Button-1>."
                    }
                }
            }
        }
    }
    subsection "Palette for FSM minimization" {
        rm "Both input and output signals may be either "
        bf "observed"
        rm " or "
        bf "hidden"
        rm ", i.e. taken and not taken into account during behavior "
        rm "comparison of states, respectively. Each signal list "
        rm "is linked to a color palette made of two colors:"
        itemize {
            item {
                bf "black"
                rm ", for observed;"
            }
            item {
                bf "grey"
                rm ", for hidden."
            }
        }
    }
    subsection "Palette for Output Signal Emission Checking" {
        rm "Inputs signals can be given a fixed value or let free:"
        itemize {
            item {
                bf "black"
                rm ", to let the signal have any value;"
            }
            item {
                bf "blue"
                rm ", to fix the signal to 0 (always absent)"
            }
            item {
                bf "red"
                rm ", to fix the signal to 1 (always present)"
            }
        }
        par "Output signal have to be selected for emission checking:"
        itemize {
            item {
                bf "black"
                rm ", not selected;"
            }
            item {
                bf "blue"
                rm ", to check the signal is possibly not emitted"
            }
            item {
                bf "red"
                rm ", to check the signal is possibly emitted"
            }
        }
    }
}

section "FSM Reduction and Visualization" {
    mark "FSM Reduction and Visualization"
    rm "Xeve uses an equivalence called "
    it "bisimulation"
    rm ". Roughly speaking, this equivalence relates states that are "
    rm "not distinguishable when exploring the FSM graph. Reduction "
    rm "of FSMs consists in collapsing equivalent states and "
    rm "building the underlying quotient. The equivalence can be "
    rm "widened by hiding un-relevant signals with respect to the "
    rm "observation you want to make. Hiding inputs may introduce "
    rm "nondeterministic behavior. Still, bisimulation gives "
    rm "a minimal canonical form for non deterministic FSMs and has "
    rm "an efficient polynomial time algorithm."
    par "Minimized FSMs are generated explicitly and saved in ascii "
    rm "files using the "
    bf "Fc2"
    rm " format. This format is the entry format of "
    bf "Atg"
    rm ", the graphical tool for FSM exploration and visualization."
    cr
    par "To apply minimization, select the \"REDUCE\" radiobutton and set "
    rm "the signals you want to observe as well as the ones you want to hide. "
    rm "Invoke the \"Apply\" button. A file browser appears asking you for "
    rm "a file name in which to save the minimized FSM. After file selection, "
    rm "a result window is popped-up to displayed the evolution of the "
    rm "computation and its results."
    par "Buttons are provided to abort the "
    rm "computation (\"Abort\") if it takes too much time, to dismiss the "
    rm "result window once the computation is complete (\"Dismiss\"), and "
    rm "a button to invoke the FSM graphical visualization "
    rm "(\"Draw Automaton\")."
}

section "Observers and Output Emission Checking" {
    mark "Observers and Output Emission Checking"
    rm "A way to verify temporal properties like safety or liveness ones, "
    rm "is to put an observer that catches misbehaviors and property "
    rm "violation from the program to verify. Typical properties are in the "
    rm "form "
    it "if SIGNAL1 and SIGNAL2 are present then emit PROPERTY_VIOLATED"
    rm ", or "
    it "if SIGNAL1 is present then before k occurrences of SIGNAL2, SIGNAL3 "
    it "must be emitted, otherwise emit PROPERTY_VIOLATED"
    rm ". The observer is in fact another Esterel program put in parallel "
    rm "with the main one."
    cr
    par "To perform such verification, input the FSM of an "
    it "observed"
    rm " program, i.e. a program compiled with a set of observers put in "
    rm "parallel. Select the \"CHECK OUTPUTS\" radiobutton. Then you may "
    rm "put constraints on the inputs signal by fixing the values of some "
    rm "of them (coloring to blue those to fix to 0, to red those to fix to "
    rm "1, to black those to let free). Select the output signal you want to "
    rm "check if they are possibly emitted (red) or possibly not emitted "
    rm "(blue). Invoke the \"Apply\" button. A result window is popped-up to "
    rm "displayed the evolution of the "
    rm "computation and its results."
    par "Buttons are provided to abort the "
    rm "computation (\"Abort\") if it takes too much time, to dismiss the "
    rm "result window once the computation is complete (\"Dismiss\"). "
    rm "Output signals to check are displayed on a listbox. Clicking on "
    rm "a signal name here shows its status if it has been checked."
}

section "Advanced Verification" {
    mark "Advanced Verification"
    rm "The advanced verification consists in verifying critical status "
    rm "of the behavior of the program. This is mainly checking the "
    rm "termination capabilities and potential infinite silent behaviors, "
    rm "i.e., with no output emission."
    subsection "Termination" {
        rm "An Esterel program may terminate. The user might expect such "
        rm "a behavior from the program. To check it, set first the "
        rm "termination predicate you want to check. There are two "
        rm "possibilities:"
        itemize {
            item {
                rm "the program "
                bf "can terminate"
                rm ", there exist an execution that leads to a program"
                rm "termination."
            }
            item {
                rm "the program "
                bf "must terminate"
                rm ", all executions lead to a program termination."
            }
        }
        rm "Choose the predicate (Can or Must) and then choose the "
        rm "\"Terminate\" property from the option menus."
        rm "Then press the \"Check\" button. A Yes/No result"
        rm "is then displayed."
    }
    subsection "Idling" {
        rm "An Esterel program may idle, i.e. it may loop forever, changing "
        rm "state at each instant, without emitting any output signal. To "
        rm "check if such a behavior exists, choose the predicate \"Can\" "
        rm "and the property \"Idle forever\". Then press the \"Check\" "
        rm "button. A Yes/No result is then displayed."
    }
}

section "Exiting" {
    mark "Exiting"
    rm "To exit Xeve, either use the menu entry \"Files:Quit\" or type"
    rm " <Control-q> anywhere on the graphical interface. In both case"
    rm " a Yes/No window message is popped-up that ask to confirm you"
    rm " really want to exit."
}

section "Credits" {
    mark "Credits"
    bf "Tcl/Tk"
    rm " is developed at Scriptics (http://www.scriptics.com/)"
    cr
    par
    bf "TiGeR"
    rm " is a DEC product commercially distributed by Xorix, developed by "
    rm "O. Coudert, J.C. Madre, H. Touati"
    cr
    par
    bf "The balloon"
    rm " help system is a modified version of an initial "
    rm "implementation in TkDesk by Christian Bolik "
    rm "(zzhibol@rrzn-user.uni-hannover.de)."
    cr
    par
    bf "This help"
    rm " is a modified version of an initial implementation in the "
    rm "Jstools by Jay Sekora (js@priceton.edu)."
}


global aboutSections
global aboutContents
set aboutContents {}

set aboutSections(Name) "about"
set aboutSections(Title) "About Xeve"

lappend aboutContents {Info command}
set aboutSections(Info) {get_info}



