#include "rtInt.h"#include "rt.h"#include "ntm.h"#include "part.h"#include <errno.h>#include <math.h>
Include dependency graph for rtMain.c:
Go to the source code of this file.
Functions | |
| static int | CommandRt (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static RtConfigs_t * | Rt_ReadConfigFile (char *filename) |
| static char * | Rt_SplitLine (char *command, int *argc, char ***argv) |
| static int | Rt_CompareResult (RtConfigs_t *config, RtDesignLists_t *designList, int refOnly) |
| static int | Rt_WriteBatchCommand (RtConfigs_t *config, RtDesignLists_t *designList) |
| static int | Rt_ExecuteVis (RtConfigs_t *config, RtDesignLists_t *designList, int refAndNew, FILE *scriptOut) |
| static int | Rt_WriteResult (RtConfigs_t *config, int size) |
| static void | Rt_FreeRtConfig (RtConfigs_t *config) |
| static void | Rt_FreeCommandResult (RtCommandResults_t *result) |
| static void | Rt_FreeCompareItem (RtCompareItems_t *item) |
| static void | Rt_FreeResultProperty (RtResultPropertys_t *prop) |
| static void | Rt_FreeDesignList (RtDesignLists_t *list) |
| static void | Rt_FreeArgv (int argc, char **argv) |
| static int | Rt_ReadDesignListFile (RtConfigs_t *config) |
| static int | Rt_ReadCommandTemplate (RtConfigs_t *config) |
| static int | RtCheckInputFileAvailability (RtConfigs_t *config, RtDesignLists_t *designList, int withWarning) |
| static void | Rt_RemoveUnderscore (char *name, char *newName) |
| static int | Rt_IsNum (char *tmp) |
| static int | Rt_SetBooleanValue (char *str, char *option) |
| void | Rt_Init (void) |
| void | Rt_End (void) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: rtMain.c,v 1.36 2010/04/10 00:38:42 fabio Exp $" |
Function Documentation
| static int CommandRt | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Compare two different execution of vis and make a set of tables summarizing results.]
CommandName [regression_test]
CommandSynopsis [perform regression test with the information given in arguments file]
CommandArguments [ \[-s <script_file_name>\] ]
CommandDescription [ Invokes two set of execution of vis to compare the performance and to check sanity of each execution. Then make a set of tables summarizing results, such as CPU sec, memoty usage and fail/pass of model_check, etc.. This command will read a description of the regression test to be performed from the argument file, which is configuartion file. Besides the configuration file, one needs to prepare two template files and a design list. We now describe these in turn. As running example we shall use a regression test that compares check_invariant with and without guided search.
The configuration file for our example is shown below, delimited by lines of dashes (which are not part of the file). The order in which the lines appear in the file is immaterial. A line beginning with '#' is a comment, and is ignored by regression_test.
----------------------------------------------------------------------
DesignDirectory : /projects/development/hsv/vis/Regression
DesignList : ./DesignListInv
ReferenceVis : /usr/local/vis/i686-o/vis-cu
ReferenceVisNickName : BFS
ReferenceOutputDir : ./result_inv_bfs
RefCommandTemplate : ./TemplateRefInv
bRefRun : FALSE
NewVis : /usr/local/vis/i686-o/vis-cu
NewVisNickName : GS
NewOutputDir : ./result_inv_gs
bNewRun : FALSE
NewCommandTemplate : ./TemplateNewInv
bCompareCounterExample : TRUE
bDefaultInitCommand : FALSE
ResultForPerformance : ./BFSvsGS.tex
CompareItem : cpu : elapse:
CompareItem : mem : Memory in use:
CompareItem : bdd : Peak number of live nodes:
----------------------------------------------------------------------
Each line defines a parameter of the regression test.
* DesignDirectory gives the path to the directory where the input files are stored. In this case, we are using the central repository under ~hsv/vis/Regression. It's typically a good idea to store the results of regression tests in a separate place from the input files. In our examples, the results are stored in the current directory.
* DesignList gives the name of the file containing the list of test cases to run. Each line consists of several white space-separated fields describing the files making up the test case. The first field is a path to the files relative to DesignDirectory. The second field is the test case name. The remaining fields are file names. More on this later, when we talk about the design list file in detail.
* ReferenceVis and NewVis give paths to the two versions of vis to be compared in the regression test. They can be the same, as in this case in which both are the "nightly build."
* ReferenceVisNickName and NewVisNickName are two identifiers that are used in the LaTeX tables to refer to the two versions that are compared. Short mnemonics are preferable. Avoid using underscores, because they currently cause trouble with LaTeX.
* ReferenceOutputDir and NewOutputDir give the names of the directories in which the results of the runs will be stored. In each of these directories, vis_reg will create a directory for each test case. The names of these directories are the test case names taken from the design list. Therefore, these names must be unique.
* RefCommandTemplate and NewCommandTemplate are the templates from which vis_reg produces the scripts used to run the test cases. The mechanism used to derive the scripts from the templates and the design list is described in detail when we talk about the template files. The two templates can be the same file.
* bRefRun and bNewRun are flags that tell vis_reg which of the two sets of experiments should be run (if any). If one set of results has been already computed, the corresponding flag should be set to FALSE. If both flags are FALSE, vis_reg simply regenerates the summary table.
* bCompareCounterExample is a flag that instructs vis_reg to scan the output files for counterexamples and record their lengths. For each counterexample, stem and cycle length are found. If this flag is set to FALSE, counterexamples are not analyzed and the corresponding table is not produced.
* bDefaultInitCommand is a flag that, if set to TRUE, instructs vis_reg to generate a default set of commands to initialize each vis run. This option allows one to save some time in preparing the templates, at the expense of some flexibility.
* ResultForPerformance is the name of the LaTeX file to which vis_reg writes the summary of the experiments. Its format is described in detail later.
* CompareItem specifies one item to be monitored in the experiments. Multiple CompareItem lines may appear in the configuration file. Each one consists of two items: an identifier, and a pattern. The identifier is used in the table to denote the item, whereas the pattern is used to extract from the output files the information to be put in the tables.
In our example, we declare
CompareItem : mem : Memory in use:
We instruct regression_test to search for a line beginning with "Memory in use:" in each section of the output file. The token immediately following the occurrence of the pattern is the data item to be put in the table under "mem." so that the resulting LaTeX table contains data on the memmory usage.
Since the output file is divided into sections delimited by strings "CommandBegin" and "CommandEnd." (See below.), each section is searched for the patterns specified by the CompareItem declarations. If the pattern is matched, the item appears in the table for that section.
To run the regression_test we need configuration file, template file and design list. In case of template file, we need a two template files, since we want to compare two different run of vis. The syntax of the two templates is identical. We describe the template for "new," but all we say applies to "ref" as well. The "new" template for our example is shown below.
----------------------------------------------------------------------
echo CommandBegin init
read_model
flt
order_vars
part
time
print_bdd_stats
echo CommandEnd init
echo CommandBegin ci
set hd_frontier_approx_threshold 3500
ci -t 3600 -g $HintFile $InvFile
time
print_bdd_stats
echo CommandEnd ci
echo CommandBegin ci_cex
ci -d 1 -i -t 3600 -g $HintFile $InvFile
time
print_bdd_stats
echo CommandEnd ci_cex
----------------------------------------------------------------------
Before proceeding to its discussion, it is instructive to examine the script that regression_test produces from it for one test case. regression_test relies on vis's shell variables and aliases to customize the script. The script consists of a preamble in which variables and aliases are defined, followed by one or more sections, each corresponding to a major step in the experiment. Statistics will be collected for each step separately. Our example has three sections, whose names are "init," "ci," and "ci_cex." The names of the sections are arbitrary, except that the automatically generated initialization section is always called "init."
----------------------------------------------------------------------
set vis_stdout ./result_inv_gs/am2901/am2901.out
set vis_stderr ./result_inv_gs/am2901/am2901.err
set BlifFile /projects/development/hsv/vis/Regression/Am2901/am2901.mv
set OrdFile /projects/development/hsv/vis/Regression/Am2901/am2901.ord
set InvFile /projects/development/hsv/vis/Regression/Am2901/am2901.inv
set HintFile /projects/development/hsv/vis/Regression/Am2901/am2901.hint
alias read_model "rlmv $BlifFile"
alias set_fairness " "
alias order_vars "so -s input_and_latch $OrdFile"
echo CommandBegin init
read_model
flt
order_vars
part
time
print_bdd_stats
echo CommandEnd init
echo CommandBegin ci
set hd_frontier_approx_threshold 3500
ci -t 3600 -g $HintFile $InvFile
time
print_bdd_stats
echo CommandEnd ci
echo CommandBegin ci_cex
ci -d 1 -i -t 3600 -g $HintFile $InvFile
time
print_bdd_stats
echo CommandEnd ci_cex
quit
----------------------------------------------------------------------
The variables and the aliases are defined by vis_reg by examining the fields of the test case description in the design file. regression_test uses file extensions to identify file types. (E.g., .ord indicates an order file in "input_and_latch" format.) A full list of extensions is given below.
regression_test defines variables for all the file types actually available for the experiment, and only for those. It also defines three aliases that provide some flexibility in mixing different experiments in the same batch.
For instance, "read_model" is defined as either
read_blif_mv $BlifFile
or
read_blif $BlifFile
depending on whether the design list specifies a .mv file or a .blif file as model file.
The definition of "order_vars" takes into account whether an order file is available or not. Finally, the definition of "set_fairness" depends on whether a .fair file is available. This allows one to mix model checking experiments for which no fairness condition is specified to experiments that do require fairness conditions.
When bDefaultInitCommand is FALSE, the script is simply the preamble, followed by the unchanged template, follows by the "quit" command, which is always automatically added.
When bDefaultInitCommand is TRUE, regression_test also adds an automatically generated "init" section between the preamble and the template. This default section is equivalent to
echo CommandBegin init
read_model
flt
order_vars
part
time
print_bdd_stats
echo CommandEnd init
Notice that one has no control over dynamic reordering during the initialization phase if bDefaultInitCommand is TRUE.
The template should refer to the defined aliases and variables to tailor itself to each test case. Notice, however, that one is not forced to use "order_vars." If one wants to always use vis's static ordering algorithm, (s)he can simply use "so" instead of "order_vars." Likewise, one can decide to always ignore fairness constraints by not including "set_fairness."
On the other hand, it is usually a bad idea to explicitly include commands like
read_blif_mv
read_blif
so -s input_and_latch
read_fairness
in the templates, because they limit the range of test cases to which they can be applied.
As we said, the templates, and hence the scripts, are divided in sections. Each section begins and ends with an "echo" command. These commands write delimiters to the output file, which are used by vis_reg to define the scope of the pattern searches. It is important that the tag specified in corresponding pairs of CommandBegin and CommandEnd be the same.
The calls to "print_bdd_stats" are typically used to add to the output files the information requested by the CompareItem declarations. It is a good idea to specify timeouts for potentially expensive steps.
The design list file has one line for each test case. A master design list is in ~hsv/vis/Regression/DesignList. Specific design lists can be obtained by commenting out or deleting lines from this master list. One can also create an entirely new list according to the following rules.
Lines starting with '#' are interpreted as comments and are skipped, as in all files read by vis_reg.
A test case is a named collection of related files that can be used to run one or more experiments. As mentioned before, each line consists of white space-separated fields. The first is a (relative) path, while the second is the collection name. The remaining fields specify the files in the collection.
The smallest collection will specify one .mv or one .blif file. This file is called the "model file," and should always appear in the third field of the line. If the model file is the only file specified, one can run reachability analysis, but not much more. Vis_reg understands the file extensions shown in the following table. For each extension, the variable bound to the file name and a short explanation are given.
.mv $BlifFile model file to be read with rlmv
.blif $BlifFile model file to be read with rl
.ord $OrdFIle order file to be read with so -s input_and_latch
.inv $InvFile invariant file to be read with ci
.ctl $CtlFile property file to be read with mc
.fair $FairFile fairness file to be read with rf
.hint $HintFile hint file to be read with the -g option of mc, ci, and rch
Only one file of each type can appear in the collection defining one test case. If multiple property files, or different order files are available for one model file, one has to create two test cases for that model. Different models, on the other hand, can share property files, order files, and so on. The master design list provides examples for both these situations.
It is not possible to specify both a .mv file and a .blif file for one test case. There must be exactly one model file per test case.
As was mentioned before, it is important that the name of a test case be unique in the entire batch used for a regression test. On the other hand, several test cases may share the same directory, and often do when they have some files in common.
The result summary created by regression_test is a LaTeX file consisting of several tables. There is one table with performance stats for each section of the output file. In addition, there is an optional counterexample comparison table that summarizes PASS/FAIL information for the properties and the length of counterexamples. For each failing property, the length of the stem and the length of the cycle (if applicable) are reported.
Each performance table consists of one column for the test case name, followed by as many groups of three columns as there are CompareItem declarations applicable to the section that the table summarizes.
Each group of three columns gives the data for the reference run, the data for the new run, and the improvement. Vis_reg regards smaller as better. Hence, the improvement is positive if the CPU time, memory occupation, and so on, have decreased from the reference run to the new run. The improvement is computed as
(value(ref) - value(new)) / value(ref) * 100.
Notice that this formula tends to make "new" look bad. for instance, if new is twice as fast as ref, the improvement is 50%. If ref is twice as fast, however, the "improvement" is -100%.
The results of each test case are stored in a separate directory, whose name is obtained by concatenating ReferenceOutputDir (or NewOutputDir) with the test case name. Each directory stores three files, whose names are given by the test case name concatenated with .src, .out, and .err.
* test_case_name.src stores the script used to run vis.
* test_case_name.out stores what vis writes to vis_stdout.
* test_case_name.err stores what vis writes to vis_stderr.
One has to be careful, because vis_reg will overwrite these results directories without warning if run twice with the same ReferenceOutputDir or NewOutputDir and bRefRun or bNewRun set to TRUE.
With '-s' option, you can create c-shell script file to be able to run experiments in shell. We add this option to solve the problem that are happened when your template file contains child-process by system call. ]
Comment [ One cannot compare the number of iterations to convergence with BFS to those of HD or GS, because the first is reported as "FSM depth," while the other two are reported as "computation depth."
Tables are split so that the number of rows is not too large. However, tables may be too wide. All "CompareItem" items found in one section are put in the same table.
Currently, under Linux, the datasize limit is not enforced (not systematically enforced?) for the child processes spawned by vis_reg. One has to monitor experiments that may produce very large processes, because there is a concrete risk of thrashing the machine on which the regression test is run.
One cannot create experiments that read two different property files, or two different invariant files, or that perform equivalence checking. (That would require two model files.)
]
SideEffects []
One have to use reserved words in their template file, such as $OrdFile, $BlifFile, etc.. Somehow your template file contains the reserved words that are not provied in desigl list, then skip the design.
Create result directory structure and script file that are used to run individual experiments. Each directory, whose name is obtained by concatenating ReferenceOutputDir(or NewOutputDir) with the test case name, contains test_case_name.src after executing this function.
Run vis using the executable that is obtained ReferenceVis of configuration file
Run vis using the executable that is obtained NewVis of configuration file
After running two set of experimental results, read the log file of each run and compare the results.
Write a LaTeX file summarizing the results, after running each design, so that one can see the results before finishing the whole experiments.
Write a LateX file summarizing the results.
Definition at line 455 of file rtMain.c.
{
char *configurationFile;
char *scriptFile;
RtConfigs_t *config;
RtDesignLists_t *designList;
array_t *designArr;
int i;
FILE *scriptOut;
int c;
error_init();
if(argc < 2) {
fprintf(vis_stdout, "Error : ConfigurationFile is missed\n");
return(1);
}
util_getopt_reset();
scriptFile = 0;
scriptOut = 0;
while ((c = util_getopt(argc, argv, "s:h")) != EOF) {
switch(c) {
case 's':
scriptFile = util_strsav(util_optarg);
break;
case 'h':
(void) fprintf(vis_stderr, "usage: regression_test [-h] [-s scriptfile] configuration_file\n");
(void) fprintf(vis_stderr, " -h \tprint help information\n");
(void) fprintf(vis_stderr, " -s <scriptfile>\n");
(void) fprintf(vis_stderr, " \tgenerate shell script file for regression_test\n");
return 0;
default:
(void) fprintf(vis_stderr, "usage: regression_test [-h] [-s scriptfile] configuration_file\n");
(void) fprintf(vis_stderr, " -h \tprint help information\n");
(void) fprintf(vis_stderr, " -s <scriptfile>\n");
(void) fprintf(vis_stderr, " \tgenerate shell script file for regression_test\n");
return 0;
}
}
if(scriptFile) {
if(!(scriptOut = fopen(scriptFile, "w"))) {
fprintf(vis_stdout, "Error : Can't open script file '%s'\n", scriptFile);
return(1);
}
}
configurationFile = argv[util_optind];
config = Rt_ReadConfigFile(configurationFile);
if(config == 0) return(1);
config->scriptFile = scriptFile;
if(Rt_ReadDesignListFile(config)) {
Rt_FreeRtConfig(config);
return(1);
}
if(Rt_ReadCommandTemplate(config)) {
Rt_FreeRtConfig(config);
return(1);
}
designArr = config->designListArr;
for(i=0; i<array_n(designArr); i++) {
designList = array_fetch(RtDesignLists_t *, designArr, i);
if(RtCheckInputFileAvailability(config, designList, 1)) {
fprintf(vis_stdout, "Skip the design '%s' ..(%d/%d)\n", designList->designNickName, i+1, array_n(designArr));
continue;
}
if(Rt_WriteBatchCommand(config, designList)) {
fprintf(vis_stdout, "ERROR : can't write script for design '%s'\n", designList->designNickName);
continue;
}
if(Rt_ExecuteVis(config, designList, 1, scriptOut)) {
fprintf(vis_stdout, "ERROR : can't execute '%s' for design '%s'\n", config->referenceVisNickName, designList->designNickName);
}
if(Rt_ExecuteVis(config, designList, 2, scriptOut)) {
fprintf(vis_stdout, "ERROR : can't execute '%s' for design '%s'\n", config->newVisNickName, designList->designNickName);
}
if(Rt_CompareResult(config, designList, config->bRefOnly)) {
fprintf(vis_stdout, "ERROR : can't compare result for design '%s'\n", designList->designNickName);
}
fprintf(vis_stdout, "%s complete.. (%d/%d)\n", designList->designNickName, i+1, array_n(designArr));
if(config->scriptFile == 0) {
if(config->bRefRun || config->bNewRun)
Rt_WriteResult(config, i+1);
}
}
if(config->scriptFile == 0)
if(Rt_WriteResult(config, array_n(designArr))) return(1);
alarm(0);
Rt_FreeRtConfig(config);
if(scriptOut) fclose(scriptOut);
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int Rt_CompareResult | ( | RtConfigs_t * | config, |
| RtDesignLists_t * | designList, | ||
| int | refOnly | ||
| ) | [static] |
Function********************************************************************
Synopsis [Read the log file of both runs, and then store the information in the internal data structure. ]
Description [Read the log file of runs, Current version supports reachability analysis, CTL model checking and invariant checking. If that is not the case, it may read the log file without errors except the couterexample trace.]
Comment []
SideEffects []
Compile the log file based on keywords, such as CommandEnd, CommandBegin, # MC: formula, etc,. If timeout case is detected the fill the data structure with 'TimeOut'.
Definition at line 1496 of file rtMain.c.
{
FILE *fin1, *fin2;
char filename1[1024], filename2[1024];
char line[1024], *next;
RtCompareItems_t *item, *newItem;
RtResultPropertys_t *rProperty;
RtCommandResults_t *cResult;
int argc;
char **argv;
int i, len;
int propertyIndex;
int formulaSummary, commandBeginFlag;
int basicLength, stemLength, cycleLength;
int propertyIndexSummary, pIndex;
int invCheckFlag;
int nLine, countLineFlag;
array_t *itemArr;
propertyIndex = -1;
basicLength = 0;
stemLength = 0;
cycleLength = 0;
invCheckFlag = 0;
propertyIndexSummary = 0;
sprintf(filename1, "%s/%s/%s.out", config->referenceOutDirectory,
designList->designNickName,
designList->designNickName);
if(!(fin1 = fopen(filename1, "r"))) {
fprintf(vis_stdout, "Error : Can't open result file '%s'\n", filename1);
return(1);
}
fin2 = 0;
if(!refOnly) {
sprintf(filename2, "%s/%s/%s.out", config->newOutDirectory,
designList->designNickName,
designList->designNickName);
if(!(fin2 = fopen(filename2, "r"))) {
fprintf(vis_stdout, "Error : Can't open result file '%s'\n", filename2);
return(1);
}
}
itemArr = config->compareItemArr;
cResult = 0;
formulaSummary = 0;
commandBeginFlag = 0;
nLine = 0;
countLineFlag = 0;
rProperty = 0;
while(fgets(line, 1024, fin1)) {
if(countLineFlag) nLine++;
if(line[0] == '\n') continue;
if(!strncasecmp(line, "CommandEnd", 10)) {
if(rProperty && countLineFlag) {
rProperty->lengthOfCounterExample = nLine;
if(rProperty->lengthOfBasic > -1) {
if(rProperty->lengthOfStem > -1)
rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
else
rProperty->lengthOfStem = rProperty->lengthOfBasic;
}
}
countLineFlag = 0;
nLine = 0;
rProperty = 0;
commandBeginFlag = 0;
}
else if(!strncasecmp(line, "CommandBegin", 12)) {
propertyIndex = -1;
rProperty = 0;
formulaSummary = 0;
commandBeginFlag = 1;
Rt_SplitLine(line, &argc, &argv);
if(designList->resultForCommandArr1 == 0)
designList->resultForCommandArr1= array_alloc(RtCommandResults_t *, 0);
cResult = ALLOC(RtCommandResults_t, 1);
cResult->resultForProperty = 0;
cResult->compareItemArr = 0;
cResult->command = strdup(argv[1]);
cResult->bTimeOut = 0;
array_insert_last(RtCommandResults_t *, designList->resultForCommandArr1,
cResult);
Rt_FreeArgv(argc, argv);
continue;
}
else if(!strncasecmp(line, "** cmd error", 12)) {
if(cResult)
cResult->error = 1;
fprintf(vis_stdout, "ERROR : Command error was found in the output '%s'\n",
designList->designNickName);
continue;
}
else if(!strncasecmp(line, "# MC: formula", 13) && !formulaSummary) {
if(rProperty && countLineFlag) {
rProperty->lengthOfCounterExample = nLine;
if(rProperty->lengthOfBasic > -1) {
if(rProperty->lengthOfStem > -1)
rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
else
rProperty->lengthOfStem = rProperty->lengthOfBasic;
}
}
countLineFlag = 0;
nLine = 0;
propertyIndex++;
Rt_SplitLine(&line[13], &argc, &argv);
rProperty = ALLOC(RtResultPropertys_t, 1);
rProperty->lengthOfBasic = -1;
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = propertyIndex;
rProperty->failOrPass = strdup(argv[0]);
if(cResult->resultForProperty == 0)
cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty);
basicLength = 1;
stemLength = 0;
cycleLength = 0;
invCheckFlag = 0;
Rt_FreeArgv(argc, argv);
continue;
}
else if((!strncasecmp(line, "# AMC: formula", 14) ||
!strncasecmp(line, "# IMC: formula", 14) ||
!strncasecmp(line, "# BMC: formula", 14) ||
!strncasecmp(line, "# ABS: formula", 14)) && !formulaSummary) {
if(rProperty && countLineFlag) {
rProperty->lengthOfCounterExample = nLine;
if(rProperty->lengthOfBasic > -1) {
if(rProperty->lengthOfStem > -1)
rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
else
rProperty->lengthOfStem = rProperty->lengthOfBasic;
}
}
countLineFlag = 0;
nLine = 0;
propertyIndex++;
Rt_SplitLine(&line[14], &argc, &argv);
rProperty = ALLOC(RtResultPropertys_t, 1);
rProperty->lengthOfBasic = -1;
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = propertyIndex;
rProperty->failOrPass = strdup(argv[0]);
if(cResult->resultForProperty == 0)
cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty);
basicLength = 1;
stemLength = 0;
cycleLength = 0;
invCheckFlag = 0;
Rt_FreeArgv(argc, argv);
continue;
}
else if(!strncasecmp(line, "# LTL_MC: formula", 17) && !formulaSummary) {
if(rProperty && countLineFlag) {
rProperty->lengthOfCounterExample = nLine;
if(rProperty->lengthOfBasic > -1) {
if(rProperty->lengthOfStem > -1)
rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
else
rProperty->lengthOfStem = rProperty->lengthOfBasic;
}
}
countLineFlag = 0;
nLine = 0;
propertyIndex++;
Rt_SplitLine(&line[17], &argc, &argv);
rProperty = ALLOC(RtResultPropertys_t, 1);
rProperty->lengthOfBasic = -1;
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = propertyIndex;
rProperty->failOrPass = strdup(argv[0]);
if(cResult->resultForProperty == 0)
cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty);
basicLength = 1;
stemLength = 0;
cycleLength = 0;
invCheckFlag = 0;
Rt_FreeArgv(argc, argv);
continue;
}
else if(!strncasecmp(line, "--Fair path stem:", 17)) {
basicLength = 0;
stemLength = 1;
cycleLength = 0;
rProperty->lengthOfInv = -1;
continue;
}
else if(!strncasecmp(line, "--Fair path cycle:", 18)) {
basicLength = 0;
stemLength = 0;
cycleLength = 1;
rProperty->lengthOfInv = -1;
continue;
}
else if(!strncasecmp(line, "# LTL_MC: fair cycle:", 21)) {
basicLength = 0;
stemLength = 0;
cycleLength = 1;
rProperty->lengthOfInv = -1;
continue;
}
else if(!strncasecmp(line, "--State ", 8)) {
if(rProperty == 0) {
fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
continue;
}
Rt_SplitLine(&line[8], &argc, &argv);
len = strlen(argv[0]);
if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
if(basicLength) rProperty->lengthOfBasic = atoi(argv[0]);
else if(stemLength) rProperty->lengthOfStem = atoi(argv[0]);
else if(cycleLength) rProperty->lengthOfCycle = atoi(argv[0]);
else if(invCheckFlag) rProperty->lengthOfInv = atoi(argv[0]);
if(stemLength || cycleLength) rProperty->lengthOfInv = -1;
Rt_FreeArgv(argc, argv);
if(countLineFlag == 0) countLineFlag = 1;
continue;
}
else if(!strncasecmp(line, "--Goes to state ", 16)) {
if(rProperty == 0) {
fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
continue;
}
Rt_SplitLine(&line[16], &argc, &argv);
len = strlen(argv[0]);
if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
if(basicLength) rProperty->lengthOfBasic = atoi(argv[0]);
else if(stemLength) rProperty->lengthOfStem = atoi(argv[0]);
else if(cycleLength) rProperty->lengthOfCycle = atoi(argv[0]);
else if(invCheckFlag) rProperty->lengthOfInv = atoi(argv[0]);
if(stemLength || cycleLength) rProperty->lengthOfInv = -1;
Rt_FreeArgv(argc, argv);
continue;
}
else if(!strncasecmp(line, "# INV: formula", 14) && formulaSummary) {
invCheckFlag = 1;
basicLength = 0;
Rt_SplitLine(&line[14], &argc, &argv);
if(cResult->resultForProperty == 0)
cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
if(array_n(cResult->resultForProperty) >= propertyIndexSummary) {
rProperty = array_fetch(RtResultPropertys_t *, cResult->resultForProperty,
propertyIndexSummary-1);
if(!rProperty) {
rProperty = ALLOC(RtResultPropertys_t, 1);
array_insert(RtResultPropertys_t *,cResult->resultForProperty,
propertyIndexSummary-1, rProperty);
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = propertyIndexSummary;
}
if(rProperty->index != propertyIndexSummary) {
fprintf(vis_stdout, "Error when compiling log file \n");
}
}
else {
rProperty = ALLOC(RtResultPropertys_t, 1);
array_insert(RtResultPropertys_t *,cResult->resultForProperty,
propertyIndexSummary-1, rProperty);
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = propertyIndexSummary;
}
if(argv[0][0] == 'f' || argv[0][0] == 'p')
rProperty->failOrPass = strdup(argv[0]);
else
rProperty->failOrPass = strdup(argv[1]);
basicLength = 0;
stemLength = 0;
cycleLength = 0;
Rt_FreeArgv(argc, argv);
propertyIndexSummary++;
continue;
}
else if(!strncasecmp(line, "# INV: formula", 14) && !formulaSummary) {
invCheckFlag = 1;
if(rProperty && countLineFlag) rProperty->lengthOfCounterExample = nLine;
countLineFlag = 0;
nLine = 0;
Rt_SplitLine(&line[14], &argc, &argv);
if(Rt_IsNum(argv[0])) {
if(cResult->resultForProperty == 0)
cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
pIndex = atoi(argv[0]);
if(array_n(cResult->resultForProperty) > pIndex) {
rProperty = array_fetch(RtResultPropertys_t *,
cResult->resultForProperty, pIndex-1);
if(!rProperty) {
rProperty = ALLOC(RtResultPropertys_t, 1);
array_insert(RtResultPropertys_t *,cResult->resultForProperty,
pIndex-1, rProperty);
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = pIndex;
}
if(rProperty->index != pIndex) {
fprintf(vis_stdout, "Error when compiling log file \n");
}
}
else {
rProperty = ALLOC(RtResultPropertys_t, 1);
array_insert(RtResultPropertys_t *,cResult->resultForProperty,
pIndex-1, rProperty);
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = pIndex;
}
if(argv[1][0] == 'f' || argv[1][0] == 'p')
rProperty->failOrPass = strdup(argv[1]);
else
rProperty->failOrPass = strdup(argv[2]);
basicLength = 0;
stemLength = 0;
cycleLength = 0;
Rt_FreeArgv(argc, argv);
}
continue;
}
else if(!strncasecmp(line, "# INV: Summary", 14)) {
if(rProperty && countLineFlag) rProperty->lengthOfCounterExample = nLine;
countLineFlag = 0;
nLine = 0;
formulaSummary = 1;
propertyIndexSummary = 1;
continue;
}
next = strstr(line, "timeout");
if(next == 0)
next = strstr(line, "Timeout");
if(next) {
if(!strncasecmp(next, "timeout occurred after", 22)) {
cResult->bTimeOut = 1;
}
else if(!strncasecmp(next, "timeout after", 14)) {
cResult->bTimeOut = 1;
}
}
for(i=0; i<array_n(itemArr); i++) {
item = array_fetch(RtCompareItems_t *, itemArr, i);
len = strlen(item->itemName);
if(!strncasecmp(item->itemName, line, len)) {
newItem = ALLOC(RtCompareItems_t, 1);
newItem->itemNickName = strdup(item->itemNickName);
newItem->itemName = 0;
newItem->value = 0;
Rt_SplitLine(&line[len], &argc, &argv);
newItem->value = strdup(argv[0]);
if(cResult->compareItemArr == 0)
cResult->compareItemArr = array_alloc(RtCompareItems_t *, 0);
array_insert_last(RtCompareItems_t *, cResult->compareItemArr, newItem);
Rt_FreeArgv(argc, argv);
break;
}
}
}
if(commandBeginFlag == 1) {
if(cResult->resultForProperty && array_n(cResult->resultForProperty) == 0)
cResult->resultForProperty = 0;
cResult->compareItemArr = 0;
}
cResult = 0;
commandBeginFlag = 0;
nLine = 0;
countLineFlag = 0;
rProperty = 0;
while(fgets(line, 1024, fin2)) {
if(countLineFlag) nLine++;
if(line[0] == '\n') continue;
if(!strncasecmp(line, "CommandEnd", 10)) {
if(rProperty && countLineFlag) {
rProperty->lengthOfCounterExample = nLine;
if(rProperty->lengthOfBasic > -1) {
if(rProperty->lengthOfStem > -1)
rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
else
rProperty->lengthOfStem = rProperty->lengthOfBasic;
}
}
countLineFlag = 0;
rProperty = 0;
nLine = 0;
commandBeginFlag = 0;
}
else if(!strncasecmp(line, "CommandBegin", 12)) {
propertyIndex = -1;
rProperty = 0;
formulaSummary = 0;
commandBeginFlag = 1;
Rt_SplitLine(line, &argc, &argv);
if(designList->resultForCommandArr2 == 0)
designList->resultForCommandArr2= array_alloc(RtCommandResults_t *, 0);
cResult = ALLOC(RtCommandResults_t, 1);
cResult->resultForProperty = 0;
cResult->compareItemArr = 0;
cResult->bTimeOut = 0;
cResult->command = strdup(argv[1]);
array_insert_last(RtCommandResults_t *, designList->resultForCommandArr2,
cResult);
Rt_FreeArgv(argc, argv);
continue;
}
else if(!strncasecmp(line, "** cmd error", 12)) {
if(cResult)
cResult->error = 1;
fprintf(vis_stdout, "ERROR : Command error was found in the output '%s'\n",
designList->designNickName);
continue;
}
else if(!strncasecmp(line, "# MC: formula", 13) && !formulaSummary) {
if(rProperty && countLineFlag) {
rProperty->lengthOfCounterExample = nLine;
if(rProperty->lengthOfBasic > -1) {
if(rProperty->lengthOfStem > -1)
rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
else
rProperty->lengthOfStem = rProperty->lengthOfBasic;
}
}
countLineFlag = 0;
nLine = 0;
propertyIndex++;
Rt_SplitLine(&line[13], &argc, &argv);
rProperty = ALLOC(RtResultPropertys_t, 1);
rProperty->lengthOfBasic = -1;
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = propertyIndex;
rProperty->failOrPass = strdup(argv[0]);
if(cResult->resultForProperty == 0)
cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty);
basicLength = 1;
stemLength = 0;
cycleLength = 0;
invCheckFlag = 0;
Rt_FreeArgv(argc, argv);
continue;
}
else if((!strncasecmp(line, "# AMC: formula", 14) ||
!strncasecmp(line, "# IMC: formula", 14) ||
!strncasecmp(line, "# BMC: formula", 14) ||
!strncasecmp(line, "# ABS: formula", 14)) && !formulaSummary) {
if(rProperty && countLineFlag) {
rProperty->lengthOfCounterExample = nLine;
if(rProperty->lengthOfBasic > -1) {
if(rProperty->lengthOfStem > -1)
rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
else
rProperty->lengthOfStem = rProperty->lengthOfBasic;
}
}
countLineFlag = 0;
nLine = 0;
propertyIndex++;
Rt_SplitLine(&line[14], &argc, &argv);
rProperty = ALLOC(RtResultPropertys_t, 1);
rProperty->lengthOfBasic = -1;
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = propertyIndex;
rProperty->failOrPass = strdup(argv[0]);
if(cResult->resultForProperty == 0)
cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty);
basicLength = 1;
stemLength = 0;
cycleLength = 0;
invCheckFlag = 0;
Rt_FreeArgv(argc, argv);
continue;
}
else if(!strncasecmp(line, "# LTL_MC: formula", 17) && !formulaSummary) {
if(rProperty && countLineFlag) {
rProperty->lengthOfCounterExample = nLine;
if(rProperty->lengthOfBasic > -1) {
if(rProperty->lengthOfStem > -1)
rProperty->lengthOfStem = rProperty->lengthOfStem+rProperty->lengthOfBasic-1;
else
rProperty->lengthOfStem = rProperty->lengthOfBasic;
}
}
countLineFlag = 0;
nLine = 0;
propertyIndex++;
Rt_SplitLine(&line[17], &argc, &argv);
rProperty = ALLOC(RtResultPropertys_t, 1);
rProperty->lengthOfBasic = -1;
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = propertyIndex;
rProperty->failOrPass = strdup(argv[0]);
if(cResult->resultForProperty == 0)
cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
array_insert_last(RtResultPropertys_t *,cResult->resultForProperty, rProperty);
basicLength = 1;
stemLength = 0;
cycleLength = 0;
invCheckFlag = 0;
Rt_FreeArgv(argc, argv);
continue;
}
else if(!strncasecmp(line, "--Fair path stem:", 17)) {
basicLength = 0;
stemLength = 1;
cycleLength = 0;
rProperty->lengthOfInv = -1;
continue;
}
else if(!strncasecmp(line, "--Fair path cycle:", 18)) {
basicLength = 0;
stemLength = 0;
cycleLength = 1;
rProperty->lengthOfInv = -1;
continue;
}
else if(!strncasecmp(line, "# LTL_MC: fair cycle:", 21)) {
basicLength = 0;
stemLength = 0;
cycleLength = 1;
rProperty->lengthOfInv = -1;
continue;
}
else if(!strncasecmp(line, "--State ", 8)) {
if(rProperty == 0) {
fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
continue;
}
Rt_SplitLine(&line[8], &argc, &argv);
len = strlen(argv[0]);
if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
if(basicLength) rProperty->lengthOfBasic = atoi(argv[0]);
else if(stemLength) rProperty->lengthOfStem = atoi(argv[0]);
else if(cycleLength) rProperty->lengthOfCycle = atoi(argv[0]);
else if(invCheckFlag) rProperty->lengthOfInv = atoi(argv[0]);
if(stemLength || cycleLength) rProperty->lengthOfInv = -1;
if(countLineFlag == 0) countLineFlag = 1;
Rt_FreeArgv(argc, argv);
continue;
}
else if(!strncasecmp(line, "--Goes to state ", 16)) {
if(rProperty == 0) {
fprintf(stdout, "ERROR : The counterexample followed without keyword\n");
continue;
}
Rt_SplitLine(&line[16], &argc, &argv);
len = strlen(argv[0]);
if(argv[0][len-1] == ':') argv[0][len-1] = '\0';
if(basicLength) rProperty->lengthOfBasic = atoi(argv[0]);
else if(stemLength) rProperty->lengthOfStem = atoi(argv[0]);
else if(cycleLength) rProperty->lengthOfCycle = atoi(argv[0]);
else if(invCheckFlag) rProperty->lengthOfInv = atoi(argv[0]);
if(stemLength || cycleLength) rProperty->lengthOfInv = -1;
Rt_FreeArgv(argc, argv);
continue;
}
else if(!strncasecmp(line, "# INV: formula", 14) && formulaSummary) {
Rt_SplitLine(&line[14], &argc, &argv);
invCheckFlag = 1;
if(cResult->resultForProperty == 0)
cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
if(array_n(cResult->resultForProperty) >= propertyIndexSummary) {
rProperty = array_fetch(RtResultPropertys_t *, cResult->resultForProperty,
propertyIndexSummary-1);
if(!rProperty) {
rProperty = ALLOC(RtResultPropertys_t, 1);
array_insert(RtResultPropertys_t *,cResult->resultForProperty,
propertyIndexSummary-1, rProperty);
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = propertyIndexSummary;
}
if(rProperty->index != propertyIndexSummary) {
fprintf(vis_stdout, "Error when compiling log file \n");
}
}
else {
rProperty = ALLOC(RtResultPropertys_t, 1);
array_insert(RtResultPropertys_t *,cResult->resultForProperty,
propertyIndexSummary-1, rProperty);
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = propertyIndexSummary;
}
if(argv[0][0] == 'f' || argv[0][0] == 'p')
rProperty->failOrPass = strdup(argv[0]);
else
rProperty->failOrPass = strdup(argv[1]);
stemLength = 0;
cycleLength = 0;
Rt_FreeArgv(argc, argv);
propertyIndexSummary++;
continue;
}
else if(!strncasecmp(line, "# INV: formula", 14) && !formulaSummary) {
invCheckFlag = 1;
if(rProperty && countLineFlag) rProperty->lengthOfCounterExample = nLine;
countLineFlag = 0;
nLine = 0;
Rt_SplitLine(&line[14], &argc, &argv);
if(Rt_IsNum(argv[0])) {
if(cResult->resultForProperty == 0)
cResult->resultForProperty = array_alloc(RtResultPropertys_t *, 0);
pIndex = atoi(argv[0]);
if(array_n(cResult->resultForProperty) > pIndex) {
rProperty = array_fetch(RtResultPropertys_t *,
cResult->resultForProperty, pIndex-1);
if(!rProperty) {
rProperty = ALLOC(RtResultPropertys_t, 1);
array_insert(RtResultPropertys_t *,cResult->resultForProperty,
pIndex-1, rProperty);
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = pIndex;
}
if(rProperty->index != pIndex) {
fprintf(vis_stdout, "Error when compiling log file \n");
}
}
else {
rProperty = ALLOC(RtResultPropertys_t, 1);
array_insert(RtResultPropertys_t *,cResult->resultForProperty,
pIndex-1, rProperty);
rProperty->lengthOfStem = -1;
rProperty->lengthOfCycle = -1;
rProperty->lengthOfInv = -1;
rProperty->lengthOfCounterExample = -1;
rProperty->index = pIndex;
}
if(argv[1][0] == 'f' || argv[1][0] == 'p')
rProperty->failOrPass = strdup(argv[1]);
else
rProperty->failOrPass = strdup(argv[2]);
stemLength = 0;
cycleLength = 0;
Rt_FreeArgv(argc, argv);
}
continue;
}
else if(!strncasecmp(line, "# INV: Summary", 14)) {
if(rProperty && countLineFlag) rProperty->lengthOfCounterExample = nLine;
countLineFlag = 0;
nLine = 0;
formulaSummary = 1;
propertyIndexSummary = 1;
continue;
}
next = strstr(line, "timeout");
if(next == 0)
next = strstr(line, "Timeout");
if(next) {
if(!strncasecmp(next, "timeout occurred after", 22)) {
cResult->bTimeOut = 1;
}
else if(!strncasecmp(next, "timeout after", 14)) {
cResult->bTimeOut = 1;
}
}
for(i=0; i<array_n(itemArr); i++) {
item = array_fetch(RtCompareItems_t *, itemArr, i);
len = strlen(item->itemName);
if(!strncasecmp(item->itemName, line, len)) {
newItem = ALLOC(RtCompareItems_t, 1);
newItem->itemNickName = strdup(item->itemNickName);
newItem->itemName = 0;
newItem->value = 0;
Rt_SplitLine(&line[len], &argc, &argv);
newItem->value = strdup(argv[0]);
if(cResult->compareItemArr == 0)
cResult->compareItemArr = array_alloc(RtCompareItems_t *, 0);
array_insert_last(RtCompareItems_t *, cResult->compareItemArr, newItem);
Rt_FreeArgv(argc, argv);
break;
}
}
}
if(commandBeginFlag == 1) {
if(cResult->resultForProperty && array_n(cResult->resultForProperty) == 0)
cResult->resultForProperty = 0;
cResult->compareItemArr = 0;
}
fclose(fin1);
fclose(fin2);
return(0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Rt_End | ( | void | ) |
| static int Rt_ExecuteVis | ( | RtConfigs_t * | config, |
| RtDesignLists_t * | designList, | ||
| int | refAndNew, | ||
| FILE * | scriptOut | ||
| ) | [static] |
Function********************************************************************
Synopsis [Exceute experiments based on 'ReferenceVis' and 'NewVis'. ]
Description [ ]
Comment []
SideEffects []
sprintf(temp, "%s -x -f %s/%s.src >& %s/%s.out", exe, dir, name, dir, name);
sprintf(temp, "%s -x -f %s/%s.src", exe, dir, name);
Definition at line 2264 of file rtMain.c.
{
char temp[1024];
char dir[1024];
char exe[1024];
char name[1024];
char srcFile[1024];
char outFile[1024];
if(refAndNew == 1 && !config->bRefRun)return(0);
if(refAndNew == 2 && !config->bNewRun)return(0);
if(refAndNew == 1) {
sprintf(dir, "%s/%s", config->referenceOutDirectory, designList->designNickName);
sprintf(exe, "%s", config->referenceVis);
sprintf(name, "%s", designList->designNickName);
}
if(refAndNew == 2) {
sprintf(dir, "%s/%s", config->newOutDirectory, designList->designNickName);
sprintf(exe, "%s", config->newVis);
sprintf(name, "%s", designList->designNickName);
}
sprintf(srcFile, "%s/%s.src", dir, name);
sprintf(outFile, "%s/%s.out", dir, name);
if(scriptOut) {
sprintf(temp, "%s -x -f %s.src >& %s.out", exe, name, name);
fprintf(scriptOut, "echo %s begin\n", designList->designNickName);
fprintf(scriptOut, "cd %s\n", dir);
fprintf(scriptOut, "%s\n", temp);
fprintf(scriptOut, "cd ../../\n");
}
else {
sprintf(temp, "%s -x -f %s/%s.src > %s/%s.out", exe, dir, name, dir, name);
if (system(temp))
return(1);
}
return(0);
}
Here is the caller graph for this function:
| static void Rt_FreeArgv | ( | int | argc, |
| char ** | argv | ||
| ) | [static] |
| static void Rt_FreeCommandResult | ( | RtCommandResults_t * | result | ) | [static] |
Definition at line 3248 of file rtMain.c.
{
array_t *itemArr;
array_t *propArr;
RtCompareItems_t *item;
RtResultPropertys_t *prop;
int i;
if(result == 0) return;
if(result->command) free(result->command);
itemArr = result->compareItemArr;
if(itemArr) {
for(i=0; i<array_n(itemArr); i++) {
item = array_fetch(RtCompareItems_t *, itemArr, i);
Rt_FreeCompareItem(item);
}
array_free(itemArr);
}
propArr = result->resultForProperty;
if(propArr) {
for(i=0; i<array_n(propArr); i++) {
prop = array_fetch(RtResultPropertys_t *, propArr, i);
Rt_FreeResultProperty(prop);
}
array_free(propArr);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void Rt_FreeCompareItem | ( | RtCompareItems_t * | item | ) | [static] |
| static void Rt_FreeDesignList | ( | RtDesignLists_t * | list | ) | [static] |
Definition at line 3208 of file rtMain.c.
{
array_t *resultArr;
RtCommandResults_t *result;
int i;
if(list == 0) return;
if(list->designDirectory) free(list->designDirectory);
if(list->designNickName) free(list->designNickName);
if(list->blifFile) free(list->blifFile);
if(list->ctlFile) free(list->ctlFile);
if(list->invFile) free(list->invFile);
if(list->leFile) free(list->leFile);
if(list->fairFile) free(list->fairFile);
if(list->hintFile) free(list->hintFile);
if(list->ordFile) free(list->ordFile);
if(list->ltlFile) free(list->ltlFile);
resultArr = list->resultForCommandArr1;
if(resultArr) {
for(i=0; i<array_n(resultArr); i++) {
result = array_fetch(RtCommandResults_t *, resultArr, i);
Rt_FreeCommandResult(result);
}
array_free(resultArr);
}
resultArr = list->resultForCommandArr2;
if(resultArr) {
for(i=0; i<array_n(resultArr); i++) {
result = array_fetch(RtCommandResults_t *, resultArr, i);
Rt_FreeCommandResult(result);
}
array_free(resultArr);
}
free(list);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void Rt_FreeResultProperty | ( | RtResultPropertys_t * | prop | ) | [static] |
| static void Rt_FreeRtConfig | ( | RtConfigs_t * | config | ) | [static] |
Definition at line 3129 of file rtMain.c.
{
int i;
RtDesignLists_t *list;
array_t *itemArr, *designArr, *resultArr;
st_table *table;
RtCompareItems_t *item;
RtCommandResults_t *result;
st_generator *gen;
char *keyWord;
if(config == 0) return;
if(config->designDirectory) free(config->designDirectory);
if(config->designList) free(config->designList);
if(config->scriptFile) free(config->scriptFile);
if(config->resultForCounterExample) free(config->resultForCounterExample);
if(config->resultForPerformance) free(config->resultForPerformance);
if(config->referenceVis) free(config->referenceVis);
if(config->referenceVisNickName) free(config->referenceVisNickName);
if(config->referenceVisOptionFile) free(config->referenceVisOptionFile);
if(config->referenceOutDirectory) free(config->referenceOutDirectory);
if(config->refCommandTemplate) free(config->refCommandTemplate);
if(config->newVis) free(config->newVis);
if(config->newVisNickName) free(config->newVisNickName);
if(config->newVisOptionFile) free(config->newVisOptionFile);
if(config->newOutDirectory) free(config->newOutDirectory);
if(config->newCommandTemplate) free(config->newCommandTemplate);
itemArr = config->compareItemArr;
if(itemArr) {
for(i=0; i<array_n(itemArr); i++) {
item = array_fetch(RtCompareItems_t *, itemArr, i);
Rt_FreeCompareItem(item);
}
array_free(itemArr);
}
designArr = config->designListArr;
if(designArr) {
for(i=0; i<array_n(designArr); i++) {
list = array_fetch(RtDesignLists_t *, designArr, i);
Rt_FreeDesignList(list);
}
array_free(designArr);
}
resultArr = config->refCommandTemplateArr;
if(resultArr) {
for(i=0; i<array_n(resultArr); i++) {
result = array_fetch(RtCommandResults_t *, resultArr, i);
Rt_FreeCommandResult(result);
}
array_free(resultArr);
}
resultArr = config->newCommandTemplateArr;
if(resultArr) {
for(i=0; i<array_n(resultArr); i++) {
result = array_fetch(RtCommandResults_t *, resultArr, i);
Rt_FreeCommandResult(result);
}
array_free(resultArr);
}
if(config->keyWordTable) {
table = config->keyWordTable;
st_foreach_item(table, gen, &keyWord, NIL(char *)) {
free(keyWord);
}
st_free_table(table);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void Rt_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initialize mc package]
SideEffects []Function********************************************************************
Synopsis [Initialize rt package]
SideEffects []
Definition at line 115 of file rtMain.c.
{
Cmd_CommandAdd("regression_test", CommandRt, /* doesn't changes_network */ 0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int Rt_IsNum | ( | char * | tmp | ) | [static] |
Function********************************************************************
Synopsis [Check whether given string is digit or not.]
Description [ ]
Comment []
SideEffects []
Definition at line 2240 of file rtMain.c.
{
int i, len;
len = strlen(tmp);
for(i=0; i<len; i++) {
if(!isdigit((int)tmp[i]))return(0);
}
return(1);
}
Here is the caller graph for this function:
| static int Rt_ReadCommandTemplate | ( | RtConfigs_t * | config | ) | [static] |
Function********************************************************************
Synopsis [ Read command template and check whether it contains illegal command and alias. ]
Description [ When read the template, if we meet the string followed by '$', then check whether that string is reserved word or not. If the string is not reserved work then we consider that as a variable.]
Comment []
SideEffects []
Definition at line 2591 of file rtMain.c.
{
FILE *fin;
char line[1024];
char *filename;
char temp[1024];
int i;
RtCommandResults_t *cResult;
int argc;
char **argv;
char *next, *tmp;
if(config->bRefRun) {
filename = config->refCommandTemplate;
if(!(fin = fopen(filename, "r"))) {
fprintf(vis_stdout, "Error : Can't open command template file '%s' for reference\n", filename);
return(1);
}
if(config->keyWordTable == 0)
config->keyWordTable = st_init_table(strcmp, st_strhash);
config->refCommandTemplateArr = array_alloc(RtCommandResults_t *, 0);
while(fgets(line, 1024, fin)) {
if(line[0] == '#') continue;
cResult = ALLOC(RtCommandResults_t, 1);
cResult->resultForProperty = 0;
cResult->compareItemArr = 0;
cResult->command = 0;
Rt_SplitLine(line, &argc, &argv);
temp[0] = '\0';
for(i=0; i<argc; i++) {
strcat(temp, argv[i]);
if(i+1 != argc) strcat(temp, " ");
if(argv[i][0] == '$') {
if(!st_lookup(config->keyWordTable, argv[i], &tmp)) {
next = strdup(argv[i]);
st_insert(config->keyWordTable, next, next);
}
}
}
Rt_FreeArgv(argc, argv);
cResult->command = strdup(temp);
array_insert_last(RtCommandResults_t *, config->refCommandTemplateArr, cResult);
}
fclose(fin);
}
if(config->bNewRun) {
filename = config->newCommandTemplate;
if(!(fin = fopen(filename, "r"))) {
fprintf(vis_stdout, "Error : Can't open command template file '%s' for new\n", filename);
return(1);
}
if(config->keyWordTable == 0)
config->keyWordTable = st_init_table(strcmp, st_strhash);
config->newCommandTemplateArr = array_alloc(RtCommandResults_t *, 0);
while(fgets(line, 1024, fin)) {
if(line[0] == '#') continue;
cResult = ALLOC(RtCommandResults_t, 1);
cResult->resultForProperty = 0;
cResult->compareItemArr = 0;
cResult->command = 0;
Rt_SplitLine(line, &argc, &argv);
temp[0] = '\0';
for(i=0; i<argc; i++) {
strcat(temp, argv[i]);
if(i+1 != argc) strcat(temp, " ");
if(argv[i][0] == '$') {
if(!st_lookup(config->keyWordTable, argv[i], &tmp)) {
next = strdup(argv[i]);
st_insert(config->keyWordTable, next, next);
}
}
}
Rt_FreeArgv(argc, argv);
cResult->command = strdup(temp);
array_insert_last(RtCommandResults_t *, config->newCommandTemplateArr, cResult);
}
fclose(fin);
}
return(0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static RtConfigs_t * Rt_ReadConfigFile | ( | char * | filename | ) | [static] |
Function********************************************************************
Synopsis [Read Configuration file ]
Description [Read each line of Configuration file and fill the data structure. A line beginning with '#' is a comment. ]
Comment []
SideEffects []
Definition at line 2832 of file rtMain.c.
{
FILE *fin;
char line[1024];
char temp[1024];
RtConfigs_t *config;
int i, argc;
int errorFlag;
char **argv;
RtCompareItems_t *cItem;
if(!(fin = fopen(filename, "r"))) {
fprintf(vis_stdout, "Error : Can't open configuration file '%s'\n", filename);
return(0);
}
config = ALLOC(RtConfigs_t, 1);
memset(config, 0, sizeof(RtConfigs_t));
config->configurationFile = strdup(filename);
config->compareItemArr = 0;
config->bRefOnly = 0;
config->keyWordTable = 0;
config->bRefRun = -1;
config->bNewRun = -1;
while(fgets(line, 1024, fin)) {
if(line[0] == '#') continue;
if(line[0] == '\n') continue;
Rt_SplitLine(line, &argc, &argv);
if(argv[0][0] == '\n') continue;
if(argc < 3) continue;
if(argv[2] == 0) continue;
if(!strcasecmp("DesignDirectory", argv[0])) {
config->designDirectory = strdup(argv[2]);
}
else if(!strcasecmp("ReferenceVis", argv[0])) {
config->referenceVis = strdup(argv[2]);
}
else if(!strcasecmp("ReferenceVisNickName", argv[0])) {
config->referenceVisNickName = strdup(argv[2]);
}
else if(!strcasecmp("ReferenceVisOptionFile", argv[0])) {
config->referenceVisOptionFile = strdup(argv[2]);
}
else if(!strcasecmp("ReferenceOutputDir", argv[0])) {
config->referenceOutDirectory = strdup(argv[2]);
}
else if(!strcasecmp("bRefRun", argv[0])) {
config->bRefRun = Rt_SetBooleanValue(argv[2], argv[0]);
}
else if(!strcasecmp("NewVis", argv[0])) {
config->newVis = strdup(argv[2]);
}
else if(!strcasecmp("NewVisNickName", argv[0])) {
config->newVisNickName = strdup(argv[2]);
}
else if(!strcasecmp("NewVisOptionFile", argv[0])) {
config->newVisOptionFile = strdup(argv[2]);
}
else if(!strcasecmp("NewOutputDir", argv[0])) {
config->newOutDirectory = strdup(argv[2]);
}
else if(!strcasecmp("bNewRun", argv[0])) {
config->bNewRun = Rt_SetBooleanValue(argv[2], argv[0]);
}
else if(!strcasecmp("NewCommandTemplate", argv[0])) {
config->newCommandTemplate = strdup(argv[2]);
}
else if(!strcasecmp("RefCommandTemplate", argv[0])) {
config->refCommandTemplate = strdup(argv[2]);
}
else if(!strcasecmp("DesignList", argv[0])) {
config->designList = strdup(argv[2]);
}
else if(!strcasecmp("bCompareCounterExample", argv[0])) {
config->bCompareCounterExample = Rt_SetBooleanValue(argv[2], argv[0]);
}
else if(!strcasecmp("bFinalResultOnly", argv[0])) {
config->bFinalResultOnly = Rt_SetBooleanValue(argv[2], argv[0]);
}
else if(!strcasecmp("bDontRemoveTempFile", argv[0])) {
config->bDontRemoveTempFile = Rt_SetBooleanValue(argv[2], argv[0]);
}
else if(!strcasecmp("bDefaultInitCommand", argv[0])) {
config->bDefaultInitCommand = Rt_SetBooleanValue(argv[2], argv[0]);
}
else if(!strcasecmp("ResultForPerformance", argv[0])) {
config->resultForPerformance = strdup(argv[2]);
}
else if(!strcasecmp("ResultForCounterExample", argv[0])) {
config->resultForCounterExample = strdup(argv[2]);
}
else if(!strcasecmp("CompareItem", argv[0])) {
cItem = ALLOC(RtCompareItems_t, 1);
cItem->itemNickName = strdup(argv[2]);
temp[0] = '\0';
for(i=4; i<argc; i++) {
strcat(temp, argv[i]);
if(i+1 != argc) strcat(temp, " ");
}
cItem->itemName = strdup(temp);
cItem->value = 0;
if(!config->compareItemArr)
config->compareItemArr = array_alloc(RtCompareItems_t *, 0);
array_insert_last(RtCompareItems_t *, config->compareItemArr, cItem);
}
else {
fprintf(vis_stdout, "Unknown option '%s' in configuration file\n", argv[0]);
free(config);
Rt_FreeArgv(argc, argv);
fclose(fin);
return(0);
}
Rt_FreeArgv(argc, argv);
}
fclose(fin);
errorFlag = 0;
if(config->designDirectory == 0) {
fprintf(stdout, "DesignDirectory is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->referenceVis == 0) {
fprintf(stdout, "ReferenceVis is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->referenceVisNickName == 0) {
fprintf(stdout, "ReferenceVisNickName is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->referenceOutDirectory == 0) {
fprintf(stdout, "ReferenceOutDirectory is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->newVis == 0) {
fprintf(stdout, "NewVis is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->newVisNickName == 0) {
fprintf(stdout, "NewVisNickName is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->newOutDirectory == 0) {
fprintf(stdout, "NewOutDirectory is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->bRefRun == -1) {
fprintf(stdout, "bRefRun is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->bNewRun == -1) {
fprintf(stdout, "bNewRun is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->designList == 0) {
fprintf(stdout, "DesignList is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->newCommandTemplate == 0) {
fprintf(stdout, "NewCommandTemplate is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->refCommandTemplate == 0) {
fprintf(stdout, "RefCommandTemplate is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(config->compareItemArr == 0 || array_n(config->compareItemArr) == 0) {
fprintf(stdout, "CompareItem is not specified in configuration file '%s'\n",
filename);
errorFlag = 1;
}
if(errorFlag) {
free(config);
return(0);
}
return(config);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int Rt_ReadDesignListFile | ( | RtConfigs_t * | config | ) | [static] |
Function********************************************************************
Synopsis [Read the design list. ]
Description [ To specify the type of file, we use extension of file name, such as .mv, .blif, .ord, .inv, .ctl, .fair, .ltl and .hint. Each line consists of white space-separated fields. The first is a (relative) path, while the second is the collection name. The smallest collection will specify one .mv or one .blif file with path and collection name. Lines starting with '#' are interpreted as comments and are skipped, as in all files read]
Comment []
SideEffects []
Definition at line 2693 of file rtMain.c.
{
FILE *fin;
char line[1024];
char *filename, *str;
char suffix[1024];
int i, j, index, bDot, strLen;
RtDesignLists_t *designList;
int argc;
char **argv;
filename = config->designList;
if(!(fin = fopen(filename, "r"))) {
fprintf(vis_stdout, "Error : Can't open design list file '%s'\n", filename);
return(1);
}
config->designListArr = array_alloc(RtDesignLists_t *, 0);
while(fgets(line, 1024, fin)) {
if(line[0] == '#') continue;
if(line[0] == '\n') continue;
Rt_SplitLine(line, &argc, &argv);
designList = ALLOC(RtDesignLists_t, 1);
designList->designDirectory = strdup(argv[0]);
designList->designNickName = strdup(argv[1]);
designList->blifFile = strdup(argv[2]);
designList->leFile = 0;
designList->ltlFile = 0;
designList->ordFile = 0;
designList->hintFile = 0;
designList->ctlFile = 0;
designList->invFile = 0;
designList->fairFile = 0;
designList->resultForCommandArr1 = 0;
designList->resultForCommandArr2 = 0;
str = argv[2];
index = bDot = 0;
strLen = strlen(str);
for(j=strLen; j>=0; j--) {
if(str[j] == '.') {
bDot = 1;
break;
}
}
if(bDot==0) {
fprintf(vis_stdout, "Error : Missing blif or mv file in design list '%s'\n",
designList->designNickName);
Rt_FreeArgv(argc, argv);
free(designList);
continue;
}
else {
j++;
for(;str[j] != '\0'; j++) {
suffix[index++] = str[j];
}
}
suffix[index] = '\0';
if(!strcasecmp(suffix, "blif"))
designList->bIsMv = 0;
else if(!strcasecmp(suffix, "mv"))
designList->bIsMv = 1;
else {
fprintf(vis_stdout, "Error : Missing blif or mv file in design list '%s'\n",
designList->designNickName);
Rt_FreeArgv(argc, argv);
free(designList);
continue;
}
for(i=3; i<argc; i++) {
str = argv[i];
index = bDot = 0;
strLen = strlen(str);
for(j=strLen; j>=0; j--) {
if(str[j] == '.') {
bDot = 1;
break;
}
}
if(bDot==0) {
fprintf(vis_stdout, "Error : Illegal suffix of file '%s' in design list '%s'\n",
argv[i], designList->designNickName);
Rt_FreeArgv(argc, argv);
free(designList);
continue;
}
else {
j++;
for(;str[j] != '\0'; j++) {
suffix[index++] = str[j];
}
}
suffix[index] = '\0';
if(!strcasecmp(suffix, "ctl"))
designList->ctlFile = strdup(argv[i]);
else if(!strcasecmp(suffix, "fair"))
designList->fairFile = strdup(argv[i]);
else if(!strcasecmp(suffix, "inv"))
designList->invFile = strdup(argv[i]);
else if(!strcasecmp(suffix, "le"))
designList->leFile = strdup(argv[i]);
else if(!strcasecmp(suffix, "ltl"))
designList->ltlFile = strdup(argv[i]);
else if(!strcasecmp(suffix, "ord"))
designList->ordFile = strdup(argv[i]);
else if(!strcasecmp(suffix, "hint"))
designList->hintFile = strdup(argv[i]);
else {
fprintf(vis_stdout, "Illegal suffix of file '%s'\n", argv[i]);
Rt_FreeArgv(argc, argv);
fclose(fin);
return(1);
}
}
array_insert_last(RtDesignLists_t *, config->designListArr, designList);
Rt_FreeArgv(argc, argv);
}
fclose(fin);
return(0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void Rt_RemoveUnderscore | ( | char * | name, |
| char * | newName | ||
| ) | [static] |
Function********************************************************************
Synopsis [Remove underscopre from the string. ]
Description [Remove underscore from the given string, since LaTeX consider underscore as subscript keyword. ]
Comment []
SideEffects []
Definition at line 1465 of file rtMain.c.
{
int i, index ;
index = 0;
for(i=0; name[i] != '\0'; i++) {
if(name[i] == '_') {
newName[index++] = '\\';
}
newName[index++] = name[i];
}
newName[index] = '\0';
}
Here is the caller graph for this function:
| static int Rt_SetBooleanValue | ( | char * | str, |
| char * | option | ||
| ) | [static] |
Function********************************************************************
Synopsis [Return 1 if the string contains 'TURE', otherwise return 0. ]
Description [ ]
Comment []
SideEffects []
Definition at line 3036 of file rtMain.c.
{
if(!strcmp("TRUE", str) || !strcmp("1", str))
return(1);
else if(!strcmp("FALSE", str) || !strcmp("0", str))
return(0);
else {
fprintf(vis_stdout, "Warning : Illegal argement for '%s'\n", option);
fprintf(vis_stdout, " Set with default '%s : TURE'\n", option);
return(1);
}
}
Here is the caller graph for this function:
| static char * Rt_SplitLine | ( | char * | command, |
| int * | argc, | ||
| char *** | argv | ||
| ) | [static] |
Function********************************************************************
Synopsis [Split line with respect to whitespace, '#' and ';', and save individual strings in array named 'argv'. ]
Description [ ]
Comment []
SideEffects []
Definition at line 3063 of file rtMain.c.
{
register char *p, *start, c;
register int i, j;
register char *new_arg;
array_t *argv_array;
int single_quote, double_quote;
argv_array = array_alloc(char *, 5);
p = command;
for(;;) {
/* skip leading white space */
while (isspace((int)(*p))) {
p++;
}
/* skip until end of this token */
single_quote = double_quote = 0;
for(start = p; (c = *p) != '\0'; p++) {
if (c == ';' || c == '#' || isspace((int)c)) {
if (! single_quote && ! double_quote) {
break;
}
}
if (c == '\'') {
single_quote = ! single_quote;
}
if (c == '"') {
double_quote = ! double_quote;
}
}
if (single_quote || double_quote) {
(void) fprintf(vis_stderr, "** cmd warning: ignoring unbalanced quote ...\n");
}
if (start == p) break;
new_arg = ALLOC(char, p - start + 1);
j = 0;
for(i = 0; i < p - start; i++) {
c = start[i];
if ((c != '\'') && (c != '\"')) {
new_arg[j++] = isspace((int)c) ? ' ' : start[i];
}
}
new_arg[j] = '\0';
array_insert_last(char *, argv_array, new_arg);
}
*argc = array_n(argv_array);
*argv = array_data(char *, argv_array);
array_free(argv_array);
if (*p == ';') {
p++;
}
else if (*p == '#') {
for(; *p != 0; p++) ; /* skip to end of line */
}
return p;
}
Here is the caller graph for this function:
| static int Rt_WriteBatchCommand | ( | RtConfigs_t * | config, |
| RtDesignLists_t * | designList | ||
| ) | [static] |
Function********************************************************************
Synopsis [Write the script file for VIS execution. ]
Description [ Wirte the batch script for experiments. The variables and the aliases are defined by examining the fields of the test case description in the design file. It uses TemplateFile to make a script. So The template should refer to the defined aliases and variables to tailor itself to each test case. ]
Comment []
SideEffects []
fprintf(fout1, "set vis_stdout %s/%s/%s.out\n", config->referenceOutDirectory, designList->designNickName, designList->designNickName); fprintf(fout1, "set vis_stderr %s/%s/%s.out\n", config->referenceOutDirectory, designList->designNickName, designList->designNickName);
fprintf(fout2, "set vis_stdout %s/%s/%s.out\n", config->newOutDirectory, designList->designNickName, designList->designNickName); fprintf(fout2, "set vis_stderr %s/%s/%s.out\n", config->newOutDirectory, designList->designNickName, designList->designNickName);
Alias read_model, set_fairness and order_vars based on whether the design list specifies a .mv file or a .blif file as model file.
Definition at line 2330 of file rtMain.c.
{
FILE *fout1;
FILE *fout2;
char filename1[1024];
char filename2[1024];
char refDir[1024];
char temp[1024];
int i;
RtCommandResults_t *cTemplate;
array_t *cTemplateArrOld;
array_t *cTemplateArrNew;
fout1 = fout2 = 0;
if(config->bRefRun) {
sprintf(temp, "\\mkdir -p %s/%s", config->referenceOutDirectory,
designList->designNickName);
if (system(temp))
return(1);
}
if(config->bNewRun) {
sprintf(temp, "\\mkdir -p %s/%s", config->newOutDirectory,
designList->designNickName);
if (system(temp))
return(1);
}
if(config->bRefRun) {
sprintf(filename1, "%s/%s/%s.src", config->referenceOutDirectory,
designList->designNickName,
designList->designNickName);
if(!(fout1 = fopen(filename1, "w"))) {
fprintf(vis_stdout, "Error : Can't open command script file '%s'\n", filename1);
return(0);
}
}
if(config->bNewRun) {
sprintf(filename2, "%s/%s/%s.src", config->newOutDirectory,
designList->designNickName,
designList->designNickName);
if(!(fout2 = fopen(filename2, "w"))) {
fprintf(vis_stdout, "Error : Can't open command script file '%s'\n", filename2);
fclose(fout1);
return(0);
}
}
cTemplateArrOld = config->refCommandTemplateArr;
cTemplateArrNew = config->newCommandTemplateArr;
sprintf(refDir, "%s/%s", config->designDirectory, designList->designDirectory);
if(config->bRefRun) {
fprintf(fout1, "set BaseName %s\n", designList->designNickName);
}
if(config->bNewRun) {
fprintf(fout2, "set BaseName %s\n", designList->designNickName);
}
if(designList->blifFile) {
if(config->bRefRun)
fprintf(fout1, "set BlifFile %s/%s\n", refDir, designList->blifFile);
if(config->bNewRun)
fprintf(fout2, "set BlifFile %s/%s\n", refDir, designList->blifFile);
}
if(designList->ordFile) {
if(config->bRefRun)
fprintf(fout1, "set OrdFile %s/%s\n", refDir, designList->ordFile);
if(config->bNewRun)
fprintf(fout2, "set OrdFile %s/%s\n", refDir, designList->ordFile);
}
if(designList->ctlFile) {
if(config->bRefRun)
fprintf(fout1, "set CtlFile %s/%s\n", refDir, designList->ctlFile);
if(config->bNewRun)
fprintf(fout2, "set CtlFile %s/%s\n", refDir, designList->ctlFile);
}
if(designList->invFile) {
if(config->bRefRun)
fprintf(fout1, "set InvFile %s/%s\n", refDir, designList->invFile);
if(config->bNewRun)
fprintf(fout2, "set InvFile %s/%s\n", refDir, designList->invFile);
}
if(designList->leFile) {
if(config->bRefRun)
fprintf(fout1, "set LeFile %s/%s\n", refDir, designList->leFile);
if(config->bNewRun)
fprintf(fout2, "set LeFile %s/%s\n", refDir, designList->leFile);
}
if(designList->ltlFile) {
if(config->bRefRun)
fprintf(fout1, "set LtlFile %s/%s\n", refDir, designList->ltlFile);
if(config->bNewRun)
fprintf(fout2, "set LtlFile %s/%s\n", refDir, designList->ltlFile);
}
if(designList->fairFile) {
if(config->bRefRun)
fprintf(fout1, "set FairFile %s/%s\n", refDir, designList->fairFile);
if(config->bNewRun)
fprintf(fout2, "set FairFile %s/%s\n", refDir, designList->fairFile);
}
if(designList->hintFile) {
if(config->bRefRun)
fprintf(fout1, "set HintFile %s/%s\n", refDir, designList->hintFile);
if(config->bNewRun)
fprintf(fout2, "set HintFile %s/%s\n", refDir, designList->hintFile);
}
if(config->bRefRun) {
if(designList->fairFile)
fprintf(fout1, "set fairOption \"-F%s/%s\"\n", refDir, designList->fairFile);
else
fprintf(fout1, "set fairOption \" \"\n");
}
if(config->bNewRun) {
if(designList->fairFile)
fprintf(fout2, "set fairOption \"-F%s/%s\"\n", refDir, designList->fairFile);
else
fprintf(fout2, "set fairOption \" \"\n");
}
if(config->bDefaultInitCommand) {
if(config->bRefRun) {
fprintf(fout1, "echo CommandBegin init\n");
if(designList->ordFile) {
if(designList->bIsMv)
fprintf(fout1, "rlmv $BlifFile\n");
else
fprintf(fout1, "read_blif $BlifFile\n");
fprintf(fout1, "flatten_hierarchy\n");
fprintf(fout1, "static_order -s partial $OrdFile\n");
fprintf(fout1, "build_partition_mdds\n");
if(designList->fairFile)
fprintf(fout1, "rf $FairFile\n");
}
else {
if(designList->bIsMv)
fprintf(fout1, "rlmv $BlifFile\n");
else
fprintf(fout1, "read_blif $BlifFile\n");
fprintf(fout1, "echo init\n");
fprintf(fout1, "init\n");
if(designList->fairFile)
fprintf(fout1, "rf $FairFile\n");
}
fprintf(fout1, "time\n");
fprintf(fout1, "print_bdd_stats\n");
fprintf(fout1, "echo CommandEnd init\n");
}
if(config->bNewRun) {
fprintf(fout2, "echo CommandBegin init\n");
if(designList->ordFile) {
if(designList->bIsMv)
fprintf(fout2, "rlmv $BlifFile\n");
else
fprintf(fout2, "read_blif $BlifFile\n");
fprintf(fout2, "flatten_hierarchy\n");
fprintf(fout2, "static_order -s partial $OrdFile\n");
fprintf(fout2, "build_partition_mdds\n");
if(designList->fairFile)
fprintf(fout2, "rf $FairFile\n");
}
else {
if(designList->bIsMv)
fprintf(fout2, "rlmv $BlifFile\n");
else
fprintf(fout2, "read_blif $BlifFile\n");
fprintf(fout2, "echo init\n");
fprintf(fout2, "init\n");
if(designList->fairFile)
fprintf(fout2, "rf $FairFile\n");
}
fprintf(fout2, "time\n");
fprintf(fout2, "print_bdd_stats\n");
fprintf(fout2, "echo CommandEnd init\n");
}
}
else {
if(config->bRefRun) {
if(designList->bIsMv)
fprintf(fout1, "alias read_model \"rlmv $BlifFile\"\n");
else
fprintf(fout1, "alias read_model \"read_blif $BlifFile\"\n");
if(designList->fairFile)
fprintf(fout1, "alias set_fairness \"read_fairness $FairFile\"\n");
else
fprintf(fout1, "alias set_fairness \" \"\n");
if(designList->ordFile)
fprintf(fout1, "alias order_vars \"so -s input_and_latch $OrdFile\"\n");
else
fprintf(fout1, "alias order_vars \"so\"\n");
}
if(config->bNewRun) {
if(designList->bIsMv)
fprintf(fout2, "alias read_model \"rlmv $BlifFile\"\n");
else
fprintf(fout2, "alias read_model \"read_blif $BlifFile\"\n");
if(designList->fairFile)
fprintf(fout2, "alias set_fairness \"read_fairness $FairFile\"\n");
else
fprintf(fout2, "alias set_fairness \" \"\n");
if(designList->ordFile)
fprintf(fout2, "alias order_vars \"so -s input_and_latch $OrdFile\"\n");
else
fprintf(fout2, "alias order_vars \"so\"\n");
}
}
if(config->bRefRun) {
for(i=0; i<array_n(cTemplateArrOld); i++) {
cTemplate = array_fetch(RtCommandResults_t *, cTemplateArrOld, i);
fprintf(fout1, "%s\n", cTemplate->command);
}
fprintf(fout1, "quit\n");
fclose(fout1);
}
if(config->bNewRun) {
for(i=0; i<array_n(cTemplateArrNew); i++) {
cTemplate = array_fetch(RtCommandResults_t *, cTemplateArrNew, i);
fprintf(fout2, "%s\n", cTemplate->command);
}
fprintf(fout2, "quit\n");
fclose(fout2);
}
return(0);
}
Here is the caller graph for this function:
| static int Rt_WriteResult | ( | RtConfigs_t * | config, |
| int | size | ||
| ) | [static] |
Function********************************************************************
Synopsis [ Write LaTeX file summarizing results.]
Description [ The result summary created by regression_test is a LaTeX file consisting of several tables. There is one table with performance stats for each section of the output file. In addition, there is an optional counterexample comparison table that summarizes PASS/FAIL information for the properties and the length of counterexamples. For each failing property, the length of the stem and the length of the cycle (if applicable) are reported.
Each performance table consists of one column for the test case name, followed by as many groups of three columns as there are CompareItem declarations applicable to the section that the table summarizes. ]
Comment []
SideEffects []
Check whether both runs contain the same set of item, since we compare two experiments.
Write performance table header
fprintf(fout, "\\landscape\n");
If the result table have more than 31 line then split the table.
Write the property comparison table in case of model checking verification
If the result table have more than 40 line then split the table.
Write the summary of comparison
new win
ref win
tie
Definition at line 683 of file rtMain.c.
{
FILE *fout;
array_t *cResultArr, *cResultArr2;
array_t *cResultArrSample, *cItemArrSample, *cItemArrSampleMax;
array_t *cItemArr, *cItemArr2, *designArr;
array_t *pArr, *pArr2, *pArrSample;
RtCommandResults_t *cResult, *cResult2, *cResultSample;
RtCompareItems_t *cItem, *cItem2, *cItemSample;
RtDesignLists_t *designList;
RtResultPropertys_t *rProp, *rProp2;
int i, j, k, first_flag;
int property_flag;
int lineNo, estLineNo, errorFlag;
char newName[1024], endStr[10];
char newNName[1024], refNName[1024];
char newTimeout[1024], refTimeout[1024];
double value1, value2;
int lastFailedIndex;
array_t *cResultArrMax;
array_t *cItemArrMax;
double *resultArr;
double totalNum;
double gap;
pArrSample = 0;
if(!(fout = fopen(config->resultForPerformance, "w"))) {
fprintf(vis_stdout, "Error : Can't open result file '%s'\n", config->resultForPerformance);
return(1);
}
designArr = config->designListArr;
cItemArrSample = 0;
cResultArrSample = NIL(array_t);
for(k=0; k<array_n(designArr) && k<size; k++) {
designList = array_fetch(RtDesignLists_t *, designArr, k);
cResultArrSample = designList->resultForCommandArr1;
errorFlag = 0;
if(cResultArrSample) {
for(i=0; i<array_n(cResultArrSample); i++) {
cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
cItemArrSample = cResult->compareItemArr;
if(cItemArrSample == NIL(array_t)) {
errorFlag = 1;
break;
}
}
}
if(errorFlag == 0) break;
}
if(cResultArrSample == NIL(array_t)) {
fprintf(fout, "ERROR : Can't find any output for your design list\n");
fclose(fout);
return(1);
}
fprintf(fout, "\\documentclass[plain]{article}\n");
fprintf(fout, "\\usepackage{lscape}\n");
fprintf(fout, "\\begin{document}\n");
fprintf(fout, "\\setlength{\\oddsidemargin}{-0.5in}\n");
for(i=0; i<array_n(cResultArrSample); i++) {
fprintf(fout, "\\begin{table}\n");
cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
cItemArrSample = cResult->compareItemArr;
cItemArrSampleMax = cItemArrSample;
for(k=0; k<array_n(designArr) && k<size; k++) {
designList = array_fetch(RtDesignLists_t *, designArr, k);
cResultArr = designList->resultForCommandArr1;
if(cResultArr) {
if(array_n(cResultArr) > i)
cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
else
cResult = 0;
if(!cResult) continue;
cItemArrSample = cResult->compareItemArr;
if(cItemArrSample && array_n(cItemArrSample) > array_n(cItemArrSampleMax)) {
cItemArrSampleMax = cItemArrSample;
}
}
}
cItemArrSample = cItemArrSampleMax;
if(cItemArrSample == 0) {
fprintf(fout, "ERROR : Can't find any output for your design list\n");
fclose(fout);
return(1);
}
cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
Rt_RemoveUnderscore(cResult->command, newName);
Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
Rt_RemoveUnderscore(config->newVisNickName, newNName);
fprintf(fout, "\\caption{Performance Comparison Table of %s for %s(ref) and %s(new)}\n",
newName, refNName, newNName);
fprintf(fout, "\\begin{center}\n");
fprintf(fout, "\\begin{tabular}{|c||");
for(j=0; j<array_n(cItemArrSample); j++) {
fprintf(fout, "c|c|c|");
}
fprintf(fout, "} \\hline \n");
fprintf(fout, " &");
Rt_RemoveUnderscore(cResult->command, newName);
fprintf(fout, "\\multicolumn{%d}{c|}{%s} ", array_n(cItemArrSample)*3, newName);
fprintf(fout, "\\\\ \\cline{2-%d}\n", array_n(cItemArrSample)*3+1);
fprintf(fout, " &");
for(j=0; j<array_n(cItemArrSample); j++) {
cItem = array_fetch(RtCompareItems_t *, cItemArrSample, j);
if(j+1 == array_n(cItemArrSample))
fprintf(fout, "\\multicolumn{3}{c|}{%s}", cItem->itemNickName);
else
fprintf(fout, "\\multicolumn{3}{c|}{%s} &", cItem->itemNickName);
}
fprintf(fout, "\\\\ \\cline{2-%d}\n",array_n(cItemArrSample)*3+1);
fprintf(fout, "Design &");
for(j=0; j<array_n(cItemArrSample); j++) {
if(j+1 == array_n(cItemArrSample))
fprintf(fout, "ref & new & (\\%%)");
else
fprintf(fout, "ref & new & (\\%%) &");
}
fprintf(fout, "\\\\ \\hline \\hline\n");
lineNo = 0;
for(k=0; k<array_n(designArr) && k<size ; k++) {
lineNo++;
if(lineNo == 31) {
fprintf(fout, "\\end{tabular}\n");
fprintf(fout, "\\end{center}\n");
fprintf(fout, "\\end{table}\n");
fprintf(fout, "\\clearpage\n");
fprintf(fout, "\\begin{table}\n");
cResult = array_fetch(RtCommandResults_t *, cResultArrSample, i);
cItemArrSample = cResult->compareItemArr;
Rt_RemoveUnderscore(cResult->command, newName);
Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
Rt_RemoveUnderscore(config->newVisNickName, newNName);
fprintf(fout, "\\caption{Performance Comparison Table of %s for %s(ref) and %s(new)}\n",
newName, refNName, newNName);
fprintf(fout, "\\begin{center}\n");
fprintf(fout, "\\begin{tabular}{|c||");
for(j=0; j<array_n(cItemArrSample); j++) {
fprintf(fout, "c|c|c|");
}
fprintf(fout, "} \\hline \n");
fprintf(fout, " &");
Rt_RemoveUnderscore(cResult->command, newName);
fprintf(fout, "\\multicolumn{%d}{c|}{%s} ", array_n(cItemArrSample)*3, newName);
fprintf(fout, "\\\\ \\cline{2-%d}\n", array_n(cItemArrSample)*3+1);
fprintf(fout, " &");
for(j=0; j<array_n(cItemArrSample); j++) {
cItem = array_fetch(RtCompareItems_t *, cItemArrSample, j);
if(j+1 == array_n(cItemArrSample))
fprintf(fout, "\\multicolumn{3}{c|}{%s}", cItem->itemNickName);
else
fprintf(fout, "\\multicolumn{3}{c|}{%s} &", cItem->itemNickName);
}
fprintf(fout, "\\\\ \\cline{2-%d}\n",array_n(cItemArrSample)*3+1);
fprintf(fout, "Design &");
for(j=0; j<array_n(cItemArrSample); j++) {
if(j+1 == array_n(cItemArrSample))
fprintf(fout, "ref & new & (\\%%)");
else
fprintf(fout, "ref & new & (\\%%) &");
}
fprintf(fout, "\\\\ \\hline \\hline\n");
lineNo = 1;
}
designList = array_fetch(RtDesignLists_t *, designArr, k);
strcpy(newTimeout, "-");
strcpy(refTimeout, "-");
if(RtCheckInputFileAvailability(config, designList, 0)) {
continue;
}
cResultArr = designList->resultForCommandArr1;
cResultArr2 = designList->resultForCommandArr2;
Rt_RemoveUnderscore(designList->designNickName, newName);
fprintf(fout, "%s\t&", newName);
if(cResultArr && array_n(cResultArr) > i)
cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
else
cResult = 0;
if(cResultArr2 && array_n(cResultArr2) > i)
cResult2 = array_fetch(RtCommandResults_t *, cResultArr2, i);
else
cResult2 = 0;
if(cResult && cResult->bTimeOut) {
strcpy(refTimeout, "TimeOut");
}
if(cResult2 && cResult2->bTimeOut) {
strcpy(newTimeout, "TimeOut");
}
if(cResult)
cItemArr = cResult->compareItemArr;
else
cItemArr = 0;
if(cResult2)
cItemArr2 = cResult2->compareItemArr;
else
cItemArr2 = 0;
if(cItemArr == 0 && cItemArr2 == 0) {
fprintf(vis_stdout, "Warning : no result for design '%s'\n", designList->designNickName);
for(j=0; j<array_n(cItemArrSample); j++) {
if(j+1 == array_n(cItemArrSample))
fprintf(fout, " %s\t& %s\t& -\t", refTimeout, newTimeout);
else
fprintf(fout, " %s\t& %s\t& -\t&", refTimeout, newTimeout);
}
fprintf(fout, "\\\\ \\hline\n");
continue;
}
else if(cItemArr && cItemArr2) {
if(array_n(cItemArr) != array_n(cItemArr2)) {
fprintf(vis_stdout, "Warning : Can't make table for the compare item,\n");
fprintf(vis_stdout, " since they are different for '%s'\n", designList->designNickName);
fprintf(vis_stdout, " Please check your template file again.\n");
for(j=0; j<array_n(cItemArrSample); j++) {
if(j+1 == array_n(cItemArrSample))
fprintf(fout, " %s\t& %s\t& -\t", refTimeout, newTimeout);
else
fprintf(fout, " %s\t& %s\t& -\t&", refTimeout, newTimeout);
}
fprintf(fout, "\\\\ \\hline\n");
continue;
}
}
if(cItemArr) cItemArrSample = cItemArr;
else cItemArrSample = cItemArr2;
for(j=0; j<array_n(cItemArrSample); j++) {
if(cItemArr)
cItem = array_fetch(RtCompareItems_t *, cItemArr, j);
else
cItem = 0;
if(cItemArr2)
cItem2 = array_fetch(RtCompareItems_t *, cItemArr2, j);
else
cItem2 = 0;
if(cItem) sscanf(cItem->value, "%lf", &value1);
if(cItem2) sscanf(cItem2->value, "%lf", &value2);
endStr[0] = '\0';
if(j+1 != array_n(cItemArrSample)) {
endStr[0] = '&';
endStr[1] = '\0';
}
if(cItem2 && cItem) {
fprintf(fout, "%s\t& %s\t& %.2f\t%s", cItem->value, cItem2->value, (value1-value2)/value1*100, endStr);
}
else if(cItem) {
fprintf(fout, "%s\t& %s\t& -\t%s", cItem->value, newTimeout, endStr);
}
else if(cItem2) {
fprintf(fout, "%s\t& %s\t& -\t%s", refTimeout, cItem2->value, endStr);
}
}
fprintf(fout, "\\\\ \\hline\n");
}
fprintf(fout, "\\end{tabular}\n");
fprintf(fout, "\\end{center}\n");
fprintf(fout, "\\end{table}\n");
fprintf(fout, "\\clearpage\n");
}
property_flag = 0;
for(k=0; k<array_n(designArr) && k<size; k++) {
designList = array_fetch(RtDesignLists_t *, designArr, k);
cResultArr = designList->resultForCommandArr1;
if(cResultArr) {
for(i=0; i<array_n(cResultArr); i++) {
cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
pArr = cResult->resultForProperty;
if(pArr && array_n(pArr) > 0) {
property_flag = 1;
break;
}
}
}
cResultArr = designList->resultForCommandArr2;
if(cResultArr) {
for(i=0; i<array_n(cResultArr); i++) {
cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
pArr = cResult->resultForProperty;
if(pArr && array_n(pArr) > 0) {
property_flag = 1;
break;
}
}
}
if(property_flag) break;
}
if(property_flag == 1) {
fprintf(fout, "\\begin{table}\n");
Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
Rt_RemoveUnderscore(config->newVisNickName, newNName);
fprintf(fout, "\\caption{Property Comparison Table for %s(ref) \
and %s(new)}\n", refNName, newNName);
fprintf(fout, "\\begin{center}\n");
fprintf(fout, "\\begin{tabular}{|c||c|c||c|c|c||c|c|c||c|} \\hline\n");
fprintf(fout, " & & & \\multicolumn{3}{c||}{ Property(ref) } & \\multicolumn{3}{c||}{ Property(new) } & \\multicolumn{1}{c|}{ Remark }\\\\ \\cline{4-10}\n");
fprintf(fout, "Design & command & index & F or P & cex len & line len & F or P & cex len & line len& \\\\ \\hline\n");
lineNo = 0;
for(k=0; k<array_n(designArr) && k<size; k++) {
designList = array_fetch(RtDesignLists_t *, designArr, k);
if(RtCheckInputFileAvailability(config, designList, 0)) {
continue;
}
cResultArr = designList->resultForCommandArr1;
cResultArr2 = designList->resultForCommandArr2;
if(cResultArr == 0 && cResultArr2 == 0) {
fprintf(vis_stdout, "ERROR : '%s' didn't run properly\n", designList->designNickName);
continue;
}
else if(cResultArr == 0 ) {
cResultArrSample = cResultArr2;
}
else if(cResultArr2 == 0 ) {
cResultArrSample = cResultArr;
}
else {
cResultArrSample = cResultArr;
}
strcpy(refTimeout, "-");
strcpy(newTimeout, "-");
first_flag = 0;
for(i=0; i<array_n(cResultArrSample); i++) {
if(cResultArr && array_n(cResultArr) > i)
cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
else
cResult = 0;
if(cResultArr2 && array_n(cResultArr2) > i)
cResult2 = array_fetch(RtCommandResults_t *, cResultArr2, i);
else
cResult2 = 0;
if(cResult == 0 && cResult2 == 0) continue;
if(cResult && cResult->bTimeOut) {
strcpy(refTimeout, "TimeOut");
}
if(cResult2 && cResult2->bTimeOut) {
strcpy(newTimeout, "TimeOut");
}
else if((cResult && !cResult->resultForProperty) &&
(cResult2 && !cResult2->resultForProperty)) continue;
if(cResult)
pArr = cResult->resultForProperty;
else
pArr = 0;
if(cResult2)
pArr2 = cResult2->resultForProperty;
else
pArr2 = 0;
if((!pArr || array_n(pArr) < 1) && (!pArr2 || array_n(pArr2) < 1)) {
continue;
}
else if(pArr && array_n(pArr) >= 1) {
pArrSample = pArr;
}
else if(pArr2 && array_n(pArr2) >= 1) {
pArrSample = pArr2;
}
estLineNo = 0;
lastFailedIndex = -1;
for(j=0; j<array_n(pArrSample); j++) {
if(pArr && array_n(pArr) > j)
rProp = array_fetch(RtResultPropertys_t *, pArr, j);
else
rProp = 0;
if(pArr2 && array_n(pArr2) > j)
rProp2 = array_fetch(RtResultPropertys_t *, pArr2, j);
else
rProp2 = 0;
if((rProp && !strncasecmp(rProp->failOrPass, "pass", 4)) &&
(rProp2 && !strncasecmp(rProp2->failOrPass, "pass", 4))) {
}
else {
estLineNo++;
lastFailedIndex = j;
}
}
if(lineNo + estLineNo > 40) {
fprintf(fout, "\\hline\n");
fprintf(fout, "\\end{tabular}\n");
fprintf(fout, "\\end{center}\n");
fprintf(fout, "\\end{table}\n");
fprintf(fout, "\\clearpage\n");
fprintf(fout, "\\begin{table}\n");
Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
Rt_RemoveUnderscore(config->newVisNickName, newNName);
fprintf(fout, "\\caption{Property Comparison Table for \
%s(ref) and %s(new)}\n", refNName, newNName);
fprintf(fout, "\\begin{center}\n");
fprintf(fout, "\\begin{tabular}{|c||c|c||c|c|c||c|c|c||c|} \\hline\n");
fprintf(fout, " & & & \\multicolumn{3}{c||}{ Property(ref) } & \\multicolumn{3}{c||}{ Property(new) } & \\multicolumn{1}{c|}{ Remark }\\\\ \\cline{4-10}\n");
fprintf(fout, "Design & command & index & F or P & cex len & line len & F or P & cex len & line len& \\\\ \\hline\n");
lineNo = 0;
}
Rt_RemoveUnderscore(designList->designNickName, newName);
if(first_flag==0) {
fprintf(fout, "%s &", newName);
first_flag = 1;
}
else
fprintf(fout, " &");
for(j=0; j<array_n(pArrSample); j++) {
lineNo++;
if(pArr && array_n(pArr) > j)
rProp = array_fetch(RtResultPropertys_t *, pArr, j);
else
rProp = 0;
if(pArr2 && array_n(pArr2) > j)
rProp2 = array_fetch(RtResultPropertys_t *, pArr2, j);
else
rProp2 = 0;
if(rProp && !strncasecmp(rProp->failOrPass, "pass", 4) &&
rProp2 && !strncasecmp(rProp2->failOrPass, "pass", 4)) {
if(j==0 && estLineNo == 0) {
if(cResult)
Rt_RemoveUnderscore(cResult->command, newName);
else
Rt_RemoveUnderscore(cResult2->command, newName);
fprintf(fout, " %s & [%d] & passed & passed & - & passed & passed & - & \\\\ ", newName, rProp->index+1);
if(j+1 == array_n(pArrSample) && i+1 == array_n(cResultArrSample))
fprintf(fout, " \\hline\n");
else if(j+1 == array_n(pArrSample))
fprintf(fout, " \\cline{2-10}\n");
else if(lastFailedIndex <= j && i+1 == array_n(cResultArrSample))
fprintf(fout, " \\hline\n");
else if(lastFailedIndex <= j)
fprintf(fout, " \\cline{2-10}\n");
else
fprintf(fout, " \\cline{4-10}\n");
}
else {
lineNo--;
}
continue;
}
if(first_flag==1) {
if(cResult) {
Rt_RemoveUnderscore(cResult->command, newName);
fprintf(fout, " %s & ", newName);
}
else if(cResult2) {
Rt_RemoveUnderscore(cResult2->command, newName);
fprintf(fout, " %s & ", newName);
}
first_flag = 2;
}
else {
fprintf(fout, " & & ");
}
if(rProp) {
if(rProp->lengthOfInv != -1)
fprintf(fout, " [%d] & %s & (%d,-) & %d &", rProp->index+1, rProp->failOrPass, rProp->lengthOfInv, rProp->lengthOfCounterExample);
else if(rProp->lengthOfStem == -1 && rProp->lengthOfCycle == -1)
fprintf(fout, " [%d] & %s & - & - &", rProp->index+1, rProp->failOrPass);
else
fprintf(fout, " [%d] & %s & (%d,%d) & %d & ", rProp->index+1, rProp->failOrPass, rProp->lengthOfStem, rProp->lengthOfCycle,rProp->lengthOfCounterExample );
}
else {
if(rProp2)
fprintf(fout, " [%d] & %s & %s & - & ", rProp2->index+1, refTimeout, refTimeout);
else
fprintf(fout, " & %s & %s & - & ", refTimeout, refTimeout);
}
if(rProp2) {
if(rProp2->lengthOfInv != -1)
fprintf(fout, " %s & (%d,-) & %d ", rProp2->failOrPass,
rProp2->lengthOfInv,rProp2->lengthOfCounterExample );
else if(rProp2->lengthOfStem == -1 && rProp2->lengthOfCycle == -1)
fprintf(fout, " %s & - & - ", rProp2->failOrPass);
else
fprintf(fout, " %s & (%d,%d) & %d ", rProp2->failOrPass,
rProp2->lengthOfStem, rProp2->lengthOfCycle, rProp2->lengthOfCounterExample);
}
else {
fprintf(fout, " %s & %s & - ", newTimeout, newTimeout);
}
endStr[0] = '\0';
if(rProp2 && rProp) {
if(rProp->failOrPass == 0 && rProp2->failOrPass)
strcpy(endStr, "Check");
else if(rProp->failOrPass && rProp2->failOrPass == 0)
strcpy(endStr, "Check");
if(rProp->failOrPass == 0 && rProp2->failOrPass == 0)
strcpy(endStr, "Check");
if(strcmp(rProp->failOrPass, rProp2->failOrPass))
strcpy(endStr, "Check");
else if(rProp->lengthOfStem != rProp2->lengthOfStem)
strcpy(endStr, "Check");
else if(rProp->lengthOfCycle != rProp2->lengthOfCycle)
strcpy(endStr, "Check");
else if(rProp->lengthOfInv != rProp2->lengthOfInv)
strcpy(endStr, "Check");
}
else {
strcpy(endStr, "Check");
}
if(j+1 == array_n(pArrSample) && i+1 == array_n(cResultArrSample))
fprintf(fout, " & %s \\\\ \\hline\n",endStr);
else if(j+1 == array_n(pArrSample))
fprintf(fout, " & %s \\\\ \\cline{2-10}\n",endStr);
else if(lastFailedIndex <= j && i+1 == array_n(cResultArrSample))
fprintf(fout, " & %s \\\\ \\hline\n", endStr);
else if(lastFailedIndex <= j)
fprintf(fout, " & %s \\\\ \\cline{2-10}\n", endStr);
else
fprintf(fout, " & %s \\\\ \\cline{4-10}\n",endStr);
}
}
}
fprintf(fout, "\\end{tabular}\n");
fprintf(fout, "\\end{center}\n");
fprintf(fout, "\\end{table}\n");
fprintf(fout, "\\clearpage\n");
}
fprintf(fout, "\\begin{table}\n");
Rt_RemoveUnderscore(config->referenceVisNickName, refNName);
Rt_RemoveUnderscore(config->newVisNickName, newNName);
fprintf(fout, "\\caption{Summary for %s(ref) and %s(new)}\n", refNName, newNName);
fprintf(fout, "\\begin{center}\n");
fprintf(fout, "\\begin{tabular}{|c|c||c|c|c|c||r|r|} \\hline\n");
fprintf(fout, " command & item & \\multicolumn{4}{c||}{ %s } & \\multicolumn{2}{c|}{ geo-mean } \\\\ \\cline{3-8}\n", newNName);
fprintf(fout, " & & win & lose & tie & NA & ref & new \\\\ \\hline \\hline\n");
cResultArrMax = 0;
for(k=0; k<array_n(designArr) && k<size; k++) {
designList = array_fetch(RtDesignLists_t *, designArr, k);
cResultArr = designList->resultForCommandArr1;
if(cResultArrMax == 0) cResultArrMax = cResultArr;
else if(cResultArr && array_n(cResultArr) > array_n(cResultArrMax)) {
cResultArrMax = cResultArr;
}
}
resultArr = ALLOC(double, 6);
for(i=0; i<array_n(cResultArrMax); i++) {
cResultSample = array_fetch(RtCommandResults_t *, cResultArrMax, i);
fprintf(fout, " %s & ", cResultSample->command);
first_flag = 1;
cItemArrMax = 0;
for(k=0; k<array_n(designArr) && k<size; k++) {
designList = array_fetch(RtDesignLists_t *, designArr, k);
cResultArr = designList->resultForCommandArr1;
if(cResultArr) {
if(array_n(cResultArr) > i)
cResult = array_fetch(RtCommandResults_t *, cResultArr, i);
else
continue;
cItemArrSample = cResult->compareItemArr;
if(cItemArrMax == 0) cItemArrMax = cItemArrSample;
else if(cItemArrSample && array_n(cItemArrSample) > array_n(cItemArrMax)) {
cItemArrMax = cItemArrSample;
}
}
}
for(j=0; j<6; j++) resultArr[j] = 0.0;
resultArr[4] = 1.0;
resultArr[5] = 1.0;
for(j=0; j<array_n(cItemArrMax); j++) {
for(k=0; k<6; k++) resultArr[k] = 0.0;
resultArr[4] = 1.0;
resultArr[5] = 1.0;
cItemSample = array_fetch(RtCompareItems_t *, cItemArrMax, j);
if(first_flag) {
fprintf(fout, "%s &\n", cItemSample->itemNickName);
first_flag = 0;
}
else {
fprintf(fout, " & %s &\n", cItemSample->itemNickName);
}
for(k=0; k<array_n(designArr) && k<size; k++) {
designList = array_fetch(RtDesignLists_t *, designArr, k);
if(designList->resultForCommandArr1 == 0 ||
designList->resultForCommandArr2 == 0) {
resultArr[3] = resultArr[3] + 1.0;
continue;
}
if(array_n(designList->resultForCommandArr1) <= i ||
array_n(designList->resultForCommandArr2) <= i) {
resultArr[3] = resultArr[3] + 1.0;
continue;
}
cResult = array_fetch(RtCommandResults_t *, designList->resultForCommandArr1, i);
cResult2 = array_fetch(RtCommandResults_t *, designList->resultForCommandArr2, i);
if(cResult == 0 || cResult2 == 0) {
resultArr[3] = resultArr[3] + 1.0;
continue;
}
if(cResult->compareItemArr == 0 ||
cResult2->compareItemArr == 0) {
resultArr[3] = resultArr[3] + 1.0;
continue;
}
if(array_n(cResult->compareItemArr) <= j ||
array_n(cResult2->compareItemArr) <= j) {
resultArr[3] = resultArr[3] + 1.0;
continue;
}
cItem = array_fetch(RtCompareItems_t *, cResult->compareItemArr, j);
cItem2 = array_fetch(RtCompareItems_t *, cResult2->compareItemArr, j);
if(cItem == 0 || cItem2 == 0) {
resultArr[3] = resultArr[3] + 1.0;
continue;
}
value1 = atof(cItem->value);
value2 = atof(cItem2->value);
if(value1 > value2) gap = value2;
else gap = value1;
gap = gap * 0.02;
if(gap < 1.0) gap = 1.0;
if(value1 > value2 + gap) resultArr[0] = resultArr[0] + 1.0;
else if(value1+gap < value2) resultArr[1] = resultArr[1] + 1.0;
else resultArr[2] += 1.0;
}
totalNum = resultArr[0] + resultArr[1] + resultArr[2];
totalNum = 1.0/totalNum;
for(k=0; k<array_n(designArr) && k<size; k++) {
designList = array_fetch(RtDesignLists_t *, designArr, k);
if(designList->resultForCommandArr1 == 0 ||
designList->resultForCommandArr2 == 0) {
continue;
}
if(array_n(designList->resultForCommandArr1) <= i ||
array_n(designList->resultForCommandArr2) <= i) {
continue;
}
cResult = array_fetch(RtCommandResults_t *, designList->resultForCommandArr1, i);
cResult2 = array_fetch(RtCommandResults_t *, designList->resultForCommandArr2, i);
if(cResult == 0 || cResult2 == 0) {
continue;
}
if(cResult->compareItemArr == 0 ||
cResult2->compareItemArr == 0) {
continue;
}
if(array_n(cResult->compareItemArr) <= j ||
array_n(cResult2->compareItemArr) <= j) {
continue;
}
cItem = array_fetch(RtCompareItems_t *, cResult->compareItemArr, j);
cItem2 = array_fetch(RtCompareItems_t *, cResult2->compareItemArr, j);
if(cItem == 0 || cItem2 == 0) {
continue;
}
value1 = atof(cItem->value);
value2 = atof(cItem2->value);
if(value1 == 0.0) value1 = 1.0;
else value1 = pow(value1, totalNum);
if(value2 == 0.0) value2 = 1.0;
else value2 = pow(value2, totalNum);
resultArr[4] *= value1;
resultArr[5] *= value2;
}
if(array_n(cItemArrMax) == j+1 ) {
fprintf(fout, " %d & %d & %d & %d & %.3f & %.3f \\\\ \\hline\n",
(int)resultArr[0], (int)resultArr[1], (int)resultArr[2],
(int)resultArr[3], resultArr[4], resultArr[5]);
}
else {
fprintf(fout, " %d & %d & %d & %d & %.3f & %.3f \\\\ \\cline{2-8}\n",
(int)resultArr[0], (int)resultArr[1], (int)resultArr[2],
(int)resultArr[3], resultArr[4], resultArr[5]);
}
}
}
free(resultArr);
fprintf(fout, "\\end{tabular}\n");
fprintf(fout, "\\end{center}\n");
fprintf(fout, "\\end{table}\n");
fprintf(fout, "\\begin{itemize}\n");
Rt_RemoveUnderscore(config->configurationFile, newName);
fprintf(fout, "\\item configuration file : %s\n", newName);
Rt_RemoveUnderscore(config->designDirectory, newName);
fprintf(fout, "\\item design directory : %s\n", newName);
Rt_RemoveUnderscore(config->designList, newName);
fprintf(fout, "\\item design list : %s\n", newName);
Rt_RemoveUnderscore(config->referenceOutDirectory, newName);
fprintf(fout, "\\item reference output dir : %s\n", newName);
Rt_RemoveUnderscore(config->referenceVis, newName);
fprintf(fout, "\\item reference executable : %s\n", newName);
Rt_RemoveUnderscore(config->refCommandTemplate, newName);
fprintf(fout, "\\item reference template : %s\n", newName);
Rt_RemoveUnderscore(config->newOutDirectory, newName);
fprintf(fout, "\\item new output dir : %s\n", newName);
Rt_RemoveUnderscore(config->newVis, newName);
fprintf(fout, "\\item new executable : %s\n", newName);
Rt_RemoveUnderscore(config->newCommandTemplate, newName);
fprintf(fout, "\\item new template : %s\n", newName);
fprintf(fout, "\\end{itemize}\n");
fprintf(fout, "\\clearpage\n");
fprintf(fout, "\\end{document}\n");
fclose(fout);
fprintf(vis_stdout, "'%s' file was generated as result of regression_test\n",
config->resultForPerformance);
return(0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int RtCheckInputFileAvailability | ( | RtConfigs_t * | config, |
| RtDesignLists_t * | designList, | ||
| int | withWarning | ||
| ) | [static] |
Function********************************************************************
Synopsis [Check whether the used file in template file is available or not. ]
Description [ One have to use reserved words in their template file, such as $OrdFile, $BlifFile, $InvFile, $CtlFile, $FairFile, $HintFile and $LeFile. Somehow your template file contains the reserved words that are not provied in design list, then skip the design. ]
Comment []
SideEffects []
Definition at line 608 of file rtMain.c.
{
st_table *keyTable;
st_generator *gen;
int errorFlag;
char *keyWord;
keyTable = config->keyWordTable;
if(keyTable == 0) return(0);
errorFlag = 0;
st_foreach_item(keyTable, gen, &keyWord, NIL(char *)) {
if(!strcasecmp(keyWord, "$CtlFile") && !designList->ctlFile) {
if(withWarning)
fprintf(vis_stdout, "WARNING : Template contains the '$CtlFile', but not in design list\n");
errorFlag = 1;
}
else if(!strcasecmp(keyWord, "$OrdFile") && !designList->ordFile) {
if(withWarning)
fprintf(vis_stdout, "WARNING : Template contains the '$OrdFile', but not in design list\n");
errorFlag = 1;
}
else if(!strcasecmp(keyWord, "$InvFile")&& !designList->invFile) {
if(withWarning)
fprintf(vis_stdout, "WARNING : Template contains the '$InvFile', but not in design list\n");
errorFlag = 1;
}
else if(!strcasecmp(keyWord, "$FairFile")&& !designList->fairFile) {
if(withWarning)
fprintf(vis_stdout, "WARNING : Template contains the '$FairFile', but not in design list\n");
errorFlag = 1;
}
else if(!strcasecmp(keyWord, "$LeFile")&& !designList->leFile) {
if(withWarning)
fprintf(vis_stdout, "WARNING : Template contains the '$LeFile', but not in design list\n");
errorFlag = 1;
}
else if(!strcasecmp(keyWord, "$LtlFile")&& !designList->ltlFile) {
if(withWarning)
fprintf(vis_stdout, "WARNING : Template contains the '$LtlFile', but not in design list\n");
errorFlag = 1;
}
else if(!strcasecmp(keyWord, "$HintFile")&& !designList->hintFile) {
if(withWarning)
fprintf(vis_stdout, "WARNING : Template contains the '$HintFile', but not in design list\n");
errorFlag = 1;
}
}
if(errorFlag == 1) return(1);
else return(0);
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: rtMain.c,v 1.36 2010/04/10 00:38:42 fabio Exp $" [static] |
CFile***********************************************************************
FileName [rtMain.c]
PackageName [rt]
Synopsis [Regression Test]
Description [ This file contains the functions for regression test. The command 'regression_test' will read a description of the regression test to be performed from the argument file, and will then carry out the test. Finally, it will produce a LaTeX file with a set of tables summarizing the results.
The regression_test command can be used to compare two different versions of vis, or two different scripts on the same version of vis, or even two different scripts on two different versions of vis. regression_test spawns the version(s) of vis to be used for the experiments as child processes. It does no other computation except setting up the experiments, starting the child processes, waiting for their termination, and collecting the results.
]
Author [HoonSang Jin]
Copyright [Copyright (c) 2001-2002 The Regents of the Univ. of Colorado. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
