twostate128.cta

很好的一本书

/* 
 * project: CTA-model of parallel running simple TwoState automata.
 * modules: TwoState, System
 * author:  Dirk Beyer, 2000
 * last change: 2001-03-28 mvogel
 * 
 * Based on: Marius Bozga, Oded Maler, Amir, Pnuelli, Sergio Yovine,
 *            "Some Progress in the Symbolic Verification of Timed Automata",
 *           In O. Grumberg, editor, Proceedings of the 9th International
 *           Conference on Computer Aided Verification (CAV'97), LNCS 1254,
 *           pages 179-190, Springer Verlag, 1997,
 *
 * The model uses internal clocks in every instance of TwoState.
 * Compare with TwoState models using external clocks, signed by the
 * filename with 'extClock' postfix. 
 */

// This module represents the template for a TwoState process.
MODULE TwoState
{
  INPUT
    // l is the minimal time (lower timebound) the automaton has to
    // stay in a state, while u is the maximal time (upper timebound)
    // it has to stay.
    l:            CONST;
    u:            CONST;
 
  // Set initial state of automaton and value of clock variable c.
  INITIAL   STATE(twoState) = one
                   AND c = 0;  
    
  AUTOMATON twoState
  {
    STATE one  { INV   c + 1 <= u;  
                 TRANS { GUARD   c >= l;  
                         DO   c' = 0;  
		         GOTO two;
                       }
               }
    
    STATE two  { INV   c + 1 <= u;  
                 TRANS { GUARD   c >= l;  
	                 DO   c' = 0;  
                         GOTO one;
		       }
               }
  }
 
  LOCAL
    c:            CLOCK(13);  // (u + 1)

}

MODULE System
{
  LOCAL
    // l is the minimal time the automaton has to stay in a state,
    // while u is the maximal time it has to stay.
    l = 9       : CONST;
    u = 12      : CONST;
 
  // Instances of TwoState template.
  INST automaton1 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton2 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton3 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton4 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton5 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton6 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton7 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton8 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton9 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton10 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton11 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton12 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton13 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton14 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton15 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton16 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton17 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton18 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton19 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton20 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton21 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton22 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton23 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton24 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton25 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton26 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton27 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton28 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton29 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton30 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton31 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton32 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton33 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton34 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton35 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton36 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton37 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton38 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton39 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton40 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton41 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton42 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton43 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton44 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton45 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton46 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton47 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton48 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton49 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton50 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton51 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton52 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton53 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton54 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton55 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton56 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton57 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton58 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton59 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton60 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton61 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton62 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton63 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton64 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton65 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton66 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton67 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton68 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton69 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton70 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton71 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton72 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton73 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton74 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton75 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton76 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton77 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton78 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton79 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton80 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton81 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton82 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton83 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton84 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton85 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton86 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton87 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton88 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton89 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton90 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton91 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton92 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton93 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton94 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton95 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton96 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton97 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton98 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton99 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton100 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton101 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton102 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton103 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton104 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton105 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton106 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton107 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton108 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton109 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton110 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton111 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton112 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton113 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton114 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton115 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton116 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton117 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton118 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton119 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton120 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton121 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton122 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton123 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton124 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton125 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton126 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton127 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 

  INST automaton128 FROM TwoState WITH
  {
    l            AS l;
    u            AS u;
  } 
}



// Analysis section:
// The module name which should be checked and the type of the internal
// representation for the region of reachable configurations is specified.
REACHABILITY CHECK System
USE BDD
{
  // Declaration of region variable. 
  VAR
    reached: REGION;

  COMMANDS

    // Use On-the-fly-Reachability-Analysis.
    IF( ISREACHABLE FROM INITIALREGION TO FALSE FORWARD )
    {
      PRINT "Error.";
    }
    ELSE
    {
      PRINT "Reachable configurations calculated.";
    }
}