Vanilla-1 Translation from HUppaal to Uppaal

Technical Report

• Abstract
• for black-and-white printing: .ps.gz
• for viewing (or printing on color printers): COLOR.pdf
• BibTeX Entry

XML Grammar

Java Documentation

• Java API of Flattening Package
  Starting point is the class Flatten, that can be called from command line

        $ java -classpath vanilla-1.jar:$CLASSPATH Flatten <input.xml>
        

  This reads the XML file input.xml (the hierarchical specification) and (over-)writes the XML file output.xml (the Uppaal format).
  To make this work, you have to put vanilla-1.jar into your working directory and your classpath has to contain crimson.jar, jaxp.jar, and xalan.jar --- i.e., the JAXP 1.1 package as to be obtained from SUN here.
  
  Please note that this is development code.
  By defaul, all debugging options are switched on, so you get a lot of information to stdout.
  
  * Please do not distribute *
  
  
• JDK 1.2 API
• General Links to Java

Pacemaker Example

• The hierarchical timed automata input file pacemaker.xml
, in correspondence with document type definition huppaal-0.6.dtd.
• Result of the translation:
  For the technical report, the layout (but not the content) were post-processed by hand, here is the layouted.xml file, in correspondence with document type definition huppaal-1.5.dtd.
  (The original old-layouted.xml file corresponds to the outdated document type definition uppaal-1.4.dtd, cannot be loaded in the distributed Uppaal version).
  You can also look at the original output:
  • as output.xml (according to the document type definition uppaal-1.4.dtd)
  • as output.xta ( UPPAAL input format with graphical information)
  • as output.ta ( UPPAAL input without graphical information)
• The properties formally verified in the technical report:
  • Safetey:
    
  • safe.q - a good switch setting is -WaCd -S 0
  • Response:
    response.q - a good switch setting is -WaAd -S 0
  • Deadlock freedom:
    As mentioned in the tech-report, the system is only deadlock free if the programmer process is not allowed to terminate.
    Use
    • modification-1.ta

      modified: L13 -> L14{guard triggerVar1 == 1; },    to
      	  L13 -> L14{guard triggerVar1 == 10; },
      	      

      or
    • modification-2.ta

      modified const ALLOW_SWITCH_OFF 1;  to
               const ALLOW_SWITCH_OFF 0; 
      	      

      or
    as input files, switch settings -aA and any true property, e.g, nodeadlock.q

PHASE III Conflict

• conflict.xml HTA input file
• output.xml Vanilla-1 translation