NOTE: The web page will contain the most current version of this document. http://www.ics.uci.edu/~rosatea/sobeit_v2.html SOBEIT 2.0 by R. Scott Truesdell (tcl/tk) and Marlon Vieira (Java) July, 1999 based on Sobeit 1.x by Chang Liu DOCUMENT HISTORY 3. Copied from ~softtest/sobeit July 1, 1999 RSTruesdell 2. Copied from ~cliu1/mcc.open Jan. 3, 1998 1. This will be UCI version of SOBEIT ENVIRONMENT SETUP Required Software: Tcl/Tk 8.0 or later tix 4.0 or later Java 1.2.0 or later Solaris 2.5 or later (SunOS 5.5.1) The environment variable CLASSPATH must be set as appropriate to look for the FSA java classes. Example: setenv CLASSPATH "home/truesdel/sharedFSA:/home/truesdel/jws:." The environment variable SOBEIT_HOME must be setup as approriate to find files relative to the executable. There are several ways to set this important environment variable; here are a few: 1. Add it in your shell's initialization file (e.g. ~/.cshrc) Example: setenv SOBEIT_HOME "/home/truesdel/rosatea/sobeit" This first method is the preferred method. 2. change to the directory in which Sobeit resides and enter the command(s): # if your shell is csh, tcsh, bash: setenv SOBEIT_HOME $cwd # if your shell is sh or korn: SOBEIT_HOME=`pwd` export SOBEIT_HOME 3. Type it in before program execution. Example: setenv SOBEIT_HOME "/home/truesdel/rosatea/sobeit" TO RUN SOBEIT % module load tcl tk tix % module load java-jdk/1.2.01 # change to whichever directory in which the file "Sobeit" resides, such as: % cd /home/truesdel/rosatea/sobeit # or, since you have set the environment variable: % cd $SOBEIT_HOME % Sobeit CHANGES INCORPORATED INTO JULY, 1999 VERSION X. ExecMonitor - work started. Abandoned; will be rolled into InstrumentWF X. InstrumentW.tcl - removed references to /home/cliu1, replaced with environment variable "SOBEIT_HOME. X. InstrumentWF.tcl - new user interface for InstrumentW.tcl rolls in elements of ExecMonitor. Incomplete. --- X. OrListBuilder.tcl - interface to build up a list of oracles for multi-FSA testing. Abandoned; rolled into newExecWindow.tcl. X. newExecWindow - removes single oracle selection and replaces it with a list of oracles and a way to build that list (and edit the list) using buttons to browse directories. Eventually to replace "ExecSuiteD.tcl". X. ExecSuiteDF.tcl - replaces "ExecSuiteD.tcl". Modified extensively to allow either GIL-based or FSA-based oracles, removed hard-coded paths, and allow multiple oracles per test run. Will be merged with newExecWindow in next version. --- X. Sobeit - replaces "uci.tcl". Adds menu-selection of oracle generator type (GIL or FSA), adds "Edit Oracle" button. Disables and Activates buttons as appropriate. X. SuiteResultWF.tcl - X. globalsF.tcl - a few new globals added, old ones commented out. X. prefs.tcl - Work started. Will be a GUI for setting some global behavior of the SoBeIt program. test root directory. X. bin/runWrapper & bin/runFSAEditor - shell scripts to invoke the shared FSA from UMass engine and the UMass FSA editor. =================================================================== How to run mapper: 1. under current directory, should be a "src" directory, all source code should be there. (All to-be-instrumented files should be there.) 2. under current directory, there must be a "instrumented" directory. Otherwise, % mapper Instrumenting computer.adb ** MAIN PROGRAM ABANDONED -- EXCEPTION "NAME_ERROR" RAISED % 3. mapper could take "*.map" file names as parameters. % mapper gas_gil.map Parsing map file gas_gil.map Instrumenting computer.adb Instrumenting computer.ads Instrumenting gas_station.adb Instrumenting random.adb Instrumenting random.ads % =================================================================== * In "InstrumentW.tcl", the location of mapper is hard coded to "/home/cliu1/sobeit/mapper", the location of temporary directory is hard coded to "/tmp". * execute_automata is from ~cliu1/agile. Because it's a modified version. Return-Path: Date: Wed, 27 Aug 1997 10:29:06 -0500 From: Charles Liu To: djr@ics.uci.edu, osella@mcc.com Subject: bug in execute_automata found and fixed Reply-to: LIU@mcc.com Content-Length: 693 The bug in execute_automata is: Every boolean expression is expressed by a list of disjunctives, each disjunctive is a list of conjunctive. When evaluating the value of an expression, the code in execute_automata assumes boolean constant is a "Boolean_Const", which is one kind of conjunctive. However, in other parts of the code, empty disjunctive list is considered "false", and a disjunctive list with only one element which is an empty conjunctive list is considered "true". This makes the evaluation of an expression return wrong result when the expression is a simple "true". It's fixed now and I'll install the new version at MCC and re-run the example today. Charles *************************************8 * gil_to_dfa is from ~cliu1/omalley. Please see ~cliu1/sobeit/lib or ~cliu1/sobeit/bin for symbolic links. ************************************************ I've put a copy of the source code (in modula3) in ftp://ftp.ics.uci.edu/~omalley/agile-src.tar.gz and the solaris executables in ftp://ftp.ics.uci.edu/~omalley/agile-bin.tar.gz The binaries include m3 libraries that must be on the load path. If the stuff is in ~mcguire/agile, you'd set it up with $ setenv LD_LIBRARY_PATH ~mcguire/agile/lib $ set path = ($path ~mcguire/agile/bin) Here is the message I wrote for Debra about how to use the tools. Here is quick rundown on the tools covering their functionality and parameters. There are three tools: gil_to_dfa: converts a giled spec to an automata print_database: prints the pkl (modula3 binary format) database execute_automata: interprets the automata gil_to_dfa takes the following parameters: -noparse Don't parse field names -dot Generate DOT files instead of the pkl database -nfa Only generate nfa instead of dfa -file Use for the database file (instead of agile.pkl) -debug Print debugging messages Parsing the fields is so that fields like "forall i: { 1 .. 10 }" will generate a forall operator instead of a literal predicate name. Some of Laurie's specs need this to work because she doesn't obey the grammar for fields. The grammar is in agile/gil/src/Predicate.gr, but it is pretty simple. DOT is useful if you want to visualize the automata instead of use them as oracles. Generate the DOT files and pass them to the dot program. The reset of the parameters are pretty obvious. The spec from giled is passed in on standard input. print_database takes only the -file parameter with the same meaning. execute_automata takes the -file parameter and the list of axioms to check during runtime. It would take a little shell script to munge the interface to match with TAOS. I think the elevator oracle used a similar script. ------------------------------------------------- > > we knew GilEd was there, but my > > impression is that we don't have a version that works on any machine > > we have now. > > It should work fine on good old kleber, which is still running sunos 4.1 for > heaven's sake.