/***********************************
  (C) Copyright 1992-1993; dit/upm
  Distributed under the conditions stated in the
  TOPO General Public License (see file LICENSE)
  ***********************************/

/***********************************

  Santiago Pavon Gomez

  25-07-1990

  Help  Functions  of Command
  Interpreter Parser of value
  expressions  main program

  ************************************/


#include "listdh.h"
#include "listdout.h"
#include "limisc.h"


/******************************************************************
 *
 *  Command: Help.
 *
 *******************************************************************/

/* Rewrite_Help
 * Help of the rewrite command.
 * If h is TRUE then an extra explanation is given.
 */
void Rewrite_Help(h)
     boolean h;
{
  printTarget("  Rewrite <expression>\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Evaluates data value expressions.\n");
  }
}

/*----------------------------------------------------------------*/

/* Load_Help
 * Help of the load command.
 * If h is TRUE then an extra explanation is given.
 */
void Load_Help(h)
     boolean h;
{
  printTarget("  Load \n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Restores the specification from the source file.\n");
  }
}

/*----------------------------------------------------------------*/

/* Print_Help
 * Help of the print command.
 * If h is TRUE then an extra explanation is given.
 */
void Print_Help(h)
     boolean h;
{
  printTarget("  Print [-p] [-t] [-a] [-c] [<depth>] [<output_file>]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Prints the current behaviour.\n");
    printTarget("\n");
    printTarget("  Options:\n");
    printTarget("                 -p: Print instantiated processes.\n");
    printTarget("                 -t: Print type definition.\n");
    printTarget("                 -a: Print the whole specification.\n");
    printTarget("                 -c: Print in Common Representation format.\n");
    printTarget("                     Only inside the LITE tool.\n");
    printTarget("            <depth>: Printing depth.\n");
    printTarget("      <output_file>: Output file. Default is console.\n");
  }
}

/*----------------------------------------------------------------*/

/* Save_Help
 * Help of the save command.
 * If h is TRUE then an extra explanation is given.
 */
void Save_Help(h)
     boolean h;
{
  printTarget("  SAve [<output_file>]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Draws the behaviour pointed in the current position into \n");
    printTarget("  the specified file.\n");
  }
}

/*----------------------------------------------------------------*/

/* Data_Help
 * Help of the datatable command.
 * If h is TRUE then an extra explanation is given.
 */
void Data_Help(h)
     boolean h;
{
  printTarget("  DataTable -s|v|o|p|g [<low_limit> [<high_limit>]]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Displays the internal tables.\n");
    printTarget("\n  Options:\n");
    printTarget("                -s: Table of sorts.\n");
    printTarget("                -v: Table of variables.\n");
    printTarget("                -o: Table of operations.\n");
    printTarget("                -p: Table of processes.\n");
    printTarget("                -g: Table of gates.\n");
    printTarget("       <low_limit>: first entry shown.\n");
    printTarget("      <high_limit>: last entry shown.\n");
  }
}

/*----------------------------------------------------------------*/

/* Expand_Help
 * Help of the expand command.
 * If h is TRUE then an extra explanation is given.
 */
void Expand_Help(h)
     boolean h;
{
  printTarget("  Expand [<depth>] [-v] [-i]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Transforms the current behaviour into a \n");
    printTarget("  Extended Finite State Machine.\n\n");
    printTarget("  This transformation stops when all the possible <depth>-length \n");
    printTarget("  sequences of events have been produced.\n\n");
    printTarget("  It also looks for duplicate states.\n");
    printTarget("\n");
    printTarget("  Option -v verbose mode.\n");
    printTarget("         -i force redundant internal actions removal.\n");
  }
}

/*----------------------------------------------------------------*/

/* Free_Help
 * Help of the free command.
 * If h is TRUE then an extra explanation is given.
 */
void Free_Help(h)
     boolean h;
{
  printTarget("  FreeExpand [<depth>] [-v] [-i]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Transforms the current behaviour into a \n");
    printTarget("  Extended Finite State Machine.\n\n");
    printTarget("  This transformation stops when all the possible <depth>-length \n");
    printTarget("  sequences of events have been produced.\n\n");
    printTarget("  It doesn't look for duplicate states.\n");
    printTarget("\n");
    printTarget("  Option -v verbose mode.\n");
    printTarget("         -i force redundant internal actions removal.\n");
  }
}

/*----------------------------------------------------------------*/

/* Var_Help
 * Help of the var command.
 * If h is TRUE then an extra explanation is given.
 */
void Var_Help(h)
     boolean h;
{
  printTarget("  VarExpand [<depth>] [-v] [-i]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  VarExpand is the parameterized expansion.\n\n");
    printTarget("  It transforms the current behaviour  \n");
    printTarget("  into a parameterized Extended Finite State Machine.\n\n");
    printTarget("  Parameterized means that all the value expressions are \n");
    printTarget("  treated symbolically.\n\n");
    printTarget("  This transformation stops when all the possible <depth>-length \n");
    printTarget("  sequences of events has been produced.\n\n");
    printTarget("  It also looks for duplicate states.\n");
    printTarget("\n");
    printTarget("  Option -v verbose mode.\n");
    printTarget("         -i force redundant internal actions removal.\n");
  }
}

/*----------------------------------------------------------------*/

static void StopHelp()
{
  static char s[2]={ '\015', '\0'};
  printTarget("\n ---------------------------- press any key ----------------------------");
#ifdef MSDOS
  (void)getxkey();
#else
  (void)fgetc(stdin);
#endif
  printTarget(s);
}

/* Test_Help
 * Help of the test command.
 * If h is TRUE then an extra explanation is given.
 */
void Test_Help(h)
     boolean h;
{
  printTarget("  TestExpand [<depth>] <success_event> [<test_proc>] [-a][-d][-e][-s]\n");
  printTarget("             [-v [<states>]] [-y][-i] [-x <expected_resp> [-q]]\n");
  printTarget("             [-b <msize>] [-p <percent> [<seed>]]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Tests a specification following the Testing Equivalence definition.\n");
    printTarget("  The test process and the current behaviour are composed in parallel,\n");
    printTarget("  synchronizing in all the gates but the success_event.\n");
    printTarget("  LOLA analyses whether the executions reach the success_event or not.\n\n");
    printTarget("  Options:   <depth>: Maximum depth of the exploration.\n");
    printTarget("     <success_event>: Special event to indicate when a execution is successful.\n");
    printTarget("                      This event can only appear in the test process.\n");
    printTarget("         <test_proc>: Test process name.\n");
    printTarget("                  -a: Generate executions leading to success.\n");
    printTarget("                  -d: Generate executions leading to depth limit.\n");
    printTarget("                  -e: Generate executions leading to exits.\n");
    printTarget("                  -s: Generate executions leading to stop.\n");
    printTarget("                  -v: Verbose mode. Display status every <states> states.\n");
    printTarget("                  -y: Force analysis of all possible executions in MAY tests.\n");
    /* KJT 23/08/07: removed "StopHelp();" */
    printTarget("                  -i: Redundant internal actions are NOT removed.            \n");
    printTarget("  -x <expected_resp>: Quit exploration if this test response does not\n");
    printTarget("                      match <expected_resp> ( must, may or reject ).\n");
    printTarget("                  -q: Quit LOLA if this test response does not\n");
    printTarget("                      match <expected_resp>.\n");
    printTarget("  Options a, s, d, e, y and i must be used only to debug the specification.\n\n");
    printTarget("  Results:     REJECT: <success_event> is never reached.\n");
    printTarget("            MUST PASS: <success_event> is always reached.\n");
    printTarget("            MAY  PASS: otherwise.\n\n");
    printTarget("  Partial Test Expansion Options (non-exhaustive exploration):\n");
    printTarget("  -p <percent> <seed>: Random selection of a percentage of transitions\n");
    printTarget("                       to be explored from every state reached.\n");
    printTarget("                       <percent> ranges over 0 ( one trace exploration )\n");
    printTarget("                       and 100 ( exhaustive exploration ).\n");
    printTarget("                       <seed> is the random number generator seed.\n");
    printTarget("           -b <msize>: Heuristic state selection with <msize> Mbytes.\n\n");

  }
}

/*----------------------------------------------------------------*/

/* One_Help
 * Help of the one command.
 * If h is TRUE then an extra explanation is given.
 */
void One_Help(h)
     boolean h;
{
  printTarget("  OneExpand <depth> [<success_event> <test_proc>] [<seed> [<execs>]] [-v] [-i]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Makes a random symbolic execution of the current behaviour.\n");
    printTarget("  If <success_event> and <test_proc> are provided, then\n");
    printTarget("  the current behaviour is composed  in parallel, synchronizing\n");
    printTarget("  in all the gates but the <success_event>, with the <test_proc>,\n");
    printTarget("  and analyses a random execution. LOLA reports whether the execution\n");
    printTarget("  reaches the <success_event> or not.\n\n");
    printTarget("  Options:\n");
    printTarget("             <depth>: Maximum number of actions generated by the execution.\n");
    printTarget("     <success_event>: Execution test stops if this event is produced.\n");
    printTarget("         <test_proc>: Process to be composed in parallel with the behaviour\n");
    printTarget("                      under test.\n");
    printTarget("              <seed>: Seed of the internal random number generator.\n");
    printTarget("                      The executions are fixed for the same seed.\n");
    printTarget("             <execs>: Times the command is to be executed taking as seed\n");
    printTarget("                      the previous random number.\n");
    printTarget("                  -v: Show the transitions generated.\n");
    printTarget("                  -i: Redundant internal actions are NOT removed.\n");
    printTarget("\n");
  }
}

/*----------------------------------------------------------------*/

/* IT_Help
 * Help of the IT command.
 * If h is TRUE then an extra explanation is given.
 */
void IT_Help(h)
     boolean h;
{
  printTarget("  InterExpand [<depth>] [-d|-p] [-v]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Computes the Interleaved Expansion of the current behaviour.\n");
    printTarget("\n");
    printTarget("  Options:   <depth>: Maximum depth of synchronizations in the exploration .\n");
    printTarget("                      Default -1 ( no bound ).\n");
    printTarget("                  -d: duplicate behaviour detection.\n");
    printTarget("                  -p: parameterized duplicate behaviour detection.\n");
    printTarget("                  -v: verbose mode.\n");
  }


}

/*----------------------------------------------------------------*/

/* Stat_Help
 * Help of the stat command.
 * If h is TRUE then an extra explanation is given.
 */
void Stat_Help(h)
     boolean h;
{
  printTarget("  STAtistic\n");
  if (h==TRUE) {
    printTarget("  Display Memory and CPU consumption.\n");
    printTarget("\n");
  }
}

/*----------------------------------------------------------------*/

/* Step_Help
 * Help of the step command.
 * If h is TRUE then a longer explanation is given.
 */
void Step_Help(h)
     boolean h;
{
  printTarget("  Step [<success_event> <test_proc>] [-u <num_undos>|-t][-d]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Enter step-by-step simulation mode: the current behaviour (or the\n");
    printTarget("  composition behaviour-test) is simulated interactively step by step.\n");
    printTarget("  This mode allows to assign expressions to parameters of processes, to\n");
    printTarget("  variables in sum-expressions and variables defined in offer lists.\n\n");
/*
    printTarget("  <success_event> and <test_proc> are used to rebuild the parallel\n");
    printTarget("  composition created with 'TestExpand' or 'OneExpand'.\n");
*/

    printTarget("  -u <num_undos> constrains the number of undo's.\n");
    printTarget("  -t disables storage of the trace of states.\n");
    printTarget("  -d disables the generation of debugging information.\n\n");

    printTarget("  Available commands in Step mode:\n");
    printTarget("     <n>     : execute transition labelled <n> from the menu of transitions.\n");
    printTarget("     Menu    : menu of transitions offered at the current state.\n");
    printTarget("     Refused : menu of unsuccessful synchronizations at the current state.\n");
    printTarget("     Undo    : undo the last simulation step (back to previous state).\n");
    printTarget("     Trace   : sequence of transitions that lead to the current state.\n");
    printTarget("     Print   : print the behaviour at the current state.\n");
    printTarget("     Sync    : show the events and processes involved in a successful\n");
    printTarget("               or unsuccessful synchronization.\n");
    printTarget("     Exit    : quit simulation mode.\n");
    printTarget("     ?       : help.\n");
  }
}

/*----------------------------------------------------------------*/

/* Move_Help
 * Help of the move command.
 * If h is TRUE then an extra explanation is given.
 */
void Move_Help(h)
     boolean h;
{
  printTarget("  Move [<position>] [<position>] ... \n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Moves the behaviour cursor to another position. <Position> can be:\n\n");
    printTarget("       <number> : the line <number> of the current behaviour.\n");
    printTarget("                  Line numbers are displayed invoking 'move' without\n");
    printTarget("                  parameters. After any movement or transformation these\n");
    printTarget("                  lines are forgotten until the next 'move' command.\n");
    printTarget("              ^ : specification level.\n");
    printTarget("    <proc_name> : process definition, called <proc_name>.\n");
    printTarget("      <number>d : go down <number> LOTOS operators.\n");
    printTarget("      <number>u : go up <number> LOTOS operators.\n");
    printTarget("      <number>b : <number>-th operand (branch) of the current operator.\n\n");
    printTarget("  Examples:\n");
    printTarget("   move      : calculates the line numbers of the current behaviour and\n");
    printTarget("   mode 11   : move the cursor to the line 11.\n\n");
    printTarget("   move 7d   : advance the cursor 7 operators forward.\n");
    printTarget("   mode 1u   : move the cursor to the previous operator.\n");
    printTarget("   move 2b   : move the cursor to the second operand of the current operator.\n");
    printTarget("   move test : move the cursor to the process called 'test'.\n");
  }
}

/*----------------------------------------------------------------*/

/* Quit_Help
 * Help of the quit command.
 * If h is TRUE then an extra explanation is given.
 */
void Quit_Help(h)
     boolean h;
{
  printTarget("  Quit\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Quits LOLA.\n");
  }
}

/*----------------------------------------------------------------*/

/* Help_Help
 * Help of the help command.
 * If h is TRUE then an extra explanation is given.
 */
void Help_Help(h)
     boolean h;
{
  printTarget("  Help [<command_name>]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Describes the specified command.\n");
  }
}

/*----------------------------------------------------------------*/

/* Set_Help
 * Help of the Set command.
 * If h is TRUE then an extra explanation is given.
 */
void Set_Help(h)
     boolean h;
{
  printTarget("  Set [<variable> [<value>]]\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Set a default value for command options and pre-expansion options.\n");
    printTarget("\n");
    printTarget("  LOLA default options are controlled by customization variables.\n");
    printTarget("  With no arguments, set displays the values of all variables.\n");
    printTarget("  With the <variable> argument alone, set resets <variable> to the initial\n");
    printTarget("  default value.\n");

  }

}

/*----------------------------------------------------------------*/

/* Cmd_Help
 * Help of the Cmd command.
 * If h is TRUE then an extra explanation is given.
 */
void Cmd_Help(h)
     boolean h;
{
  printTarget("  Command <command_file>\n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Execute a LOLA command file.\n");
    printTarget("\n");
  }
}

/*----------------------------------------------------------------*/

#ifdef INVEXP

/* PI_Help
 * Help of the PI command.
 * If h is TRUE then an extra explanation is given.
 */
void PI_Help(h)
     boolean h;
{
  printTarget("  PI <gate_list> \n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Pure interleaving decomposition.\n");
    printTarget("\n");
    printTarget("  Decomposition of the current behaviour as:\n");
    printTarget("\n");
    printTarget("      P1[A1] ||| P2[A2]\n");
    printTarget("\n");
    printTarget("  where  A1 = <gate_list>\n");
    printTarget("         A2 = A - <gate_list>\n");
    printTarget("         A  = set containing all gates\n");
    printTarget("\n\n");
    printTarget("  This transformation can only be applied to behaviours\n");
    printTarget("  without data type, and formed only with gates, stop, choices and action\n");
    printTarget("  prefixes.\n\n");
    printTarget("  NOTE: Not all the behaviours can be decomposed in this way. \n\n");
  }
}

#endif /* INVEXP */

/*----------------------------------------------------------------*/

#ifdef INVEXP

/* K_Help
 * Help of the K decomposition command.
 * If h is TRUE then an extra explanation is given.
 */
void K_Help(h)
     boolean h;
{
  printTarget("  K  <gate_list_1> , <gate_list_2> \n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Visible and Invisible Communication decomposition.\n");
    printTarget("\n");
    printTarget("  Decomposition of the current behaviour as:\n");
    printTarget("\n");
    printTarget("      HIDE  AI  IN\n");
    printTarget("      P1[A1 junction AI] | [A junction AI] | P2[A2 junction AI]\n");
    printTarget("\n");
    printTarget("  where  A1 = <gate_list_1>\n");
    printTarget("         A2 = <gate_list_2>\n");
    printTarget("         A  = <gate_list_1> inters <gate_list_2>\n");
    printTarget("         AI = hidden actions\n");
    printTarget("\n\n\n");
    printTarget("  This transformation can only be applied to behaviours\n");
    printTarget("  without data type, and formed only with gates, stop, choices \n");
    printTarget("  internal actions , processes and action prefixes.\n\n");

    printTarget("  NOTE: all the behaviours can be decomposed in this way. \n\n");
  }
}

#endif /* INVEXP */

/*----------------------------------------------------------------*/

#ifdef INVEXP


/* VC_Help
 * Help of the VC command.
 * If h is TRUE then an extra explanation is given.
 */
void VC_Help(h)
     boolean h;
{
  printTarget("  VC <gate_list_1> , <gate_list_2> \n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Visible Communication decomposition.\n");
    printTarget("\n");
    printTarget("  Decomposition of the current behaviour as:\n");
    printTarget("\n");
    printTarget("      P1[A1] |[A]| P2[A2]\n");
    printTarget("\n");
    printTarget("  where  A1 = <gate_list_1>\n");
    printTarget("         A2 = <gate_list_2>\n");
    printTarget("         A  = <gate_list_1> inters <gate_list_2>\n");
    printTarget("\n\n\n");
    printTarget("  This transformation can only be applied to deterministic behaviours,\n");
    printTarget("  without data type, and formed only with gates, stop, choices \n");
    printTarget(" , action prefixes and processes. \n\n");

    printTarget("  NOTE: Not all the behaviours can be decomposed in this way. \n\n");
  }
}


#endif /* INVEXP */

/*----------------------------------------------------------------*/

#ifdef INVEXP

/* VCNR_Help
 * Help of the VCNR command.
 * If h is TRUE then an extra explanation is given.
 */
void VCNR_Help(h)
     boolean h;
{
  printTarget("  VCNR <gate_list_1> , <gate_list_2> \n");
  if (h==TRUE) {
    printTarget("\n");
    printTarget("  Visible Communication decomposition(not recursive).\n");
    printTarget("\n");
    printTarget("  Decomposition of the current behaviour as:\n");
    printTarget("\n");
    printTarget("      P1[A1] |[A]| P2[A2]\n");
    printTarget("\n");
    printTarget("  where  A1 = <gate_list_1>\n");
    printTarget("         A2 = <gate_list_2>\n");
    printTarget("         A  = <gate_list_1> inters <gate_list_2>\n");
    printTarget("\n\n\n");
    printTarget("  This transformation can only be applied to deterministic behaviours,\n");
    printTarget("  without data type, and formed only with gates, stop, choices \n");
    printTarget("  and action prefixes.\n\n");

    printTarget("  NOTE: Not all the behaviours can be decomposed in this way. \n\n");
  }
}


#endif /* INVEXP */

#ifdef XLOLA

/*----------------------------------------------------------------*/

/* Rewrite_XHelp
 * Help of the rewrite command.
 */
void Rewrite_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                REWRITE \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Evaluates data value expressions.\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");

}

/*----------------------------------------------------------------*/

/* Load_XHelp
 * Help of the load command.
 */
void Load_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                  LOAD \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Restores the specification and the library from the source files.\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}

/*----------------------------------------------------------------*/

/* Print_XHelp
 * Help of the print command.
 */
void Print_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                 PRINT \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Prints the current behaviour.\n");
  printTarget("\n");
  printTarget("  Buttons:\n\n");
  printTarget("                 process: Prints instantiated processes.\n");
  printTarget("                   types: Prints type definition.\n");
  printTarget("     whole specification: Prints the whole specification.\n");
  printTarget("\n");
  printTarget("  Options:\n\n");
  printTarget("                   Depth: Printing depth.\n");
  printTarget("                  Output: Output file. Default is Output Window.\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}


/*----------------------------------------------------------------*/

/* Save_XHelp
 * Help of the save command.
 */
void Save_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                 SAVE  \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Draws the current behaviour into the Output File.\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}

/*----------------------------------------------------------------*/

/* Data_XHelp
 * Help of the DataTable command.
 */
void Data_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                 DATATABLE  \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Displays the internal tables.\n\n");
  printTarget("  Options:\n\n");
  printTarget("         Low Limit: first entry shown.\n");
  printTarget("        High Limit: last entry shown.\n");
  printTarget("  Buttons:\n\n");
  printTarget("             sorts: Table of sorts.\n");
  printTarget("             vars : Table of variables.\n");
  printTarget("             opers: Table of operations.\n");
  printTarget("             procs: Table of processes.\n");
  printTarget("             gates: Table of gates.\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}

/*----------------------------------------------------------------*/

/* Stat_XHelp
 * Help of the Statistic command.
 */
void Stat_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                 STATISTIC  \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Display Memory and CPU consumption.\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}

/*----------------------------------------------------------------*/

/* Expand_XHelp
 * Help of the expand command.
 */
void Expand_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                EXPAND \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Transforms the current behaviour into a \n");
  printTarget("  Extended Finite State Machine.\n\n");
  printTarget("     This transformation stops when all the possible Depth-length \n");
  printTarget("  sequences of events have been produced.\n\n");
  printTarget("  Buttons:\n\n");
  printTarget("      Rem_Int_Acts: redundant internal actions are removed.\n");
  printTarget("           Verbose: indicates verbose mode.\n");
  printTarget("      Parametrized: all the value expressions are treated symbolically.\n");
  printTarget("      Dupli_States: looks for duplicated states.\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}

/*----------------------------------------------------------------*/

/* IT_XHelp
 * Help of the IT command.
 */
void IT_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                  INTER \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Interleaved Expansion.\n");
  printTarget("\n  Buttons:\n\n");
  printTarget("       Dupli_States: Duplicate behaviour detection.\n");
  printTarget("      Parameterized: Parameterized duplicate behaviour detection.\n");
  printTarget("            Verbose: Verbose mode.\n\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}

/*----------------------------------------------------------------*/

/* Test_XHelp
 * Help of the test command.
 */
void Test_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                TEST-EXPAND \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Tests a specification following the Testing Equivalence definition.\n");
  printTarget("  The test process and  the current behaviour are  composed in parallel,\n");
  printTarget("  synchronizing in all the gates but the success_event.\n\n");
  printTarget("     XLOLA analyses if the executions reach the success_event or not.\n\n");
  printTarget("  Options:\n\n");
  printTarget("            Depth: Maximum depth of the exploration.\n");
  printTarget("        Suc Event: Special event to indicate when an execution is successful.\n");
  printTarget("                   This event can only appear in the test process.\n");
  printTarget("        Test Proc: Test process name.\n\n");
  printTarget("  Buttons:\n\n");
  printTarget("          Actions: Generate executions leading to success.\n");
  printTarget("            Depth: Generate executions leading to depth limit.\n");
  printTarget("            Exits: Generate executions leading to exits.\n");
  printTarget("            Stops: Generate executions leading to stop.\n");
  printTarget("          Verbose: Verbose mode.\n");
  printTarget("    Full_explorat: Force analysis of all possible executions in MAY tests.\n");
  printTarget("   No Rem_int_Act: Redundant internal actions are NOT removed.\n\n");
  printTarget("  Results:\n\n");
  printTarget("       REJECT    :   Event Suc is never reached.\n");
  printTarget("       MUST PASS :   Event Suc is always reached.\n");
  printTarget("       MAY PASS  :   otherwise.");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}

/*----------------------------------------------------------------*/

/* One_XHelp
 * Help of the one command.
 */
void One_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                   ONE \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Makes a random symbolic execution of the current  behaviour.\n");
  printTarget("  If the Event Suc and the Test Proc are given, then the current \n");
  printTarget("  behaviour is composed  in parallel,  synchronizing  in all the \n");
  printTarget("  gates  but  the Event Suc, with  the Test Proc, and analyses a \n");
  printTarget("  random execution. XLOLA  informs whether  the execution reaches the \n");
  printTarget("  Event Suc or not.\n\n");
  printTarget("  Options:\n\n");
  printTarget("             Depth: Maximum number of actions generated by the execution.\n");
  printTarget("         Event Suc: Execution test stops if this event is produced.\n");
  printTarget("         Test Proc: Process to be composed in parallel with the behaviour\n");
  printTarget("                    under test.\n");
  printTarget("              Seed: Seed of the internal random number generator.\n");
  printTarget("                    The executions are fixed for the same seed.\n\n");
  printTarget("  Buttons:\n\n");
  printTarget("           Verbose: Shows the transitions generated.\n");
  printTarget("    No Rem_Int_Act: Redundant internal actions are NOT removed.\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}

/*----------------------------------------------------------------*/

/* Step_XHelp
 * Help of the step command.
 */
void Step_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                   STEP \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Enter into the step-by-step simulation mode: the current behaviour (or \n");
  printTarget("  the composition behaviour-test)  is simulated interactively step by step. \n");
  printTarget("  It is possible to  assign expressions to  the variable parameters  of the \n");
  printTarget("  processes,  to the variables  in  sum-expressions and  to  the  variables \n");
  printTarget("  defined in offer or exits lists.\n\n");
  printTarget("     <success_event>  and  <test_proc>  are used  to  rebuild  the parallel \n");
  printTarget("  composition created with 'TestExpand' or 'OneExpand'.\n\n");
  printTarget("  Buttons:\n\n");
  printTarget("        Menu : Menu of transitions offered at the current  state.  Show  the \n");
  printTarget("               events and processes involved in a successful synchronization.\n");
  printTarget("               \n");
  printTarget("               Click to select an input from the  Transition  Selection \n");
  printTarget("               Window. \n");
  printTarget("     Refused : Menu of  unsuccessful  synchronizations  at the current state. \n");
  printTarget("               Show  the  events  and  processes  involved  in a unsuccessful  \n");
  printTarget("               synchronization.  Click to  select  an input from the  \n");
  printTarget("               Unsuccessful Synchronization Selection Window. \n");
  printTarget("        Undo : Undo the last simulation step (back to previous state).\n");
  printTarget("       Trace : Sequence of transitions that lead to the current state.\n");
  printTarget("       Print : Print the behaviour at the current state.\n");
  printTarget("        Exit : Quit simulation mode.\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}

/*----------------------------------------------------------------*/

/* Quit_XHelp
 * Help of the quit command.
 */
void Quit_XHelp()
{
  printTarget("\n\n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("                                   QUIT \n");
  printTarget("----------------------------------------------------------------------------\n");
  printTarget("\n\n");
  printTarget("     Quits XLOLA.\n");
  printTarget("\n\n");
  printTarget("                           *********************\n\n");
  printTarget("\n\n");
}

#endif /* XLOLA */

