The Tempo User Interface Manual
Contents
1. ii 2 send Int a do States io 0 value Int E ee Transitions E 2 send i i Trajectories J Tasks A E D Components os PF 2 invariant of A BE Outline Se sl E e Transitions al E sen El invariant of A S value gt D value Ki Console 1 error 0 warnings 0 infos Description Resource Path Location 3 E Errors 1 item undefined expression identifier something Sample tioa My Specs line 17 By default the error markers attached to a file are updated each time the file is saved This behavior is called Check Automatically The project context menu can be used to change the build behavior File Edit Navigate Window Tools Help rile 16 gt J OQQQQQl gt OHEAa Za ei SY F Sample tioa 23 Sautomaton Source au ue New gt Go Into ad Open in New Window Ri s Copy a Paste XK Delete Move Rename s Import r Export 2 Refresh Close Project Glose Unrelated Projects p Outline Properties gt wR send F increment E Q Destination Ep Signature i 2 send Int E e States Pg 9 value Int g Transitions pod send EE Trajectories J Tasks A E Dd Components Lon 2 invariant of A Check As You T2. Tempo lol x File Edit Navigate Window Tools Help l c 04000NQ gt ALA A O E sample tioa 23 _ E B87 Sautomaton Source al um gt signature E pd New output send n Int I B Go Into internal increment Rt Open in New Window states value Int O gt transitions E Copy output send n Bi Paste pre n value 6 Delete internal incremen t Move ff value value 1 Rename 5 automaton Destination i Import signature input send n Int L Export states value Int 0 a transitions E Refresh input sendin Close Project eff value n Close Unrelated Projects z Check As You Type maces A as a men z Check Automatically mponents S Source D Destination Properties E riant of A S value gt D value send F increment t Fa Trajectories Kij i Y Tasks E console 53 Problems Ex A FIN E a E Q Destinatior e EH signature plese Sp Mg Aj 2 send Int El amp Stat value Int E ee Transitions 2 send Trajectories JE Tasks EN a El Components i o 5 Ly terre oe 2 invariant of A RAET 4 My Specs 3 8 Using Tempo Tools The Tools menu allows access to other tools in the Tempo Toolset that provide assistance for more extensive checking After selecting one of the tools from the menu the active example will be executed with that tool The resulting output will be printed in the Console view ar JjOMARAAa 2 Sample tioa 23 Sautomaton Source
3. O comps i GS Schedule xa l The debugger is initiated by clicking on the simulation tool icon Once the debugger is running the arrow in the left margin of the editor window will indicate which part of the model is currently 11 being executed A break point can be added or removed by double clicking in the left margin When a break point is reached the simulation will pause and the details of the current state of the simulation can be viewed in the variables view Navigator E Variables X E is CompositeAutomaton lt C gt compa BasicAutomaton lt 4 gt dummy Int compB BasicAutomaton lt B gt dummy Int While in this paused state the debugger toolbar is used to resume step step into step out or end the simulation PAY The Simulator s Debugger has several configuration options which are not available at the command line o x type Filter text Simulator Gy pS General Install Update V Debug Tempo Plugins Start Mode LaTex ic Run Model Checker F Step PYS Simulator Formals File Browse Export Yocabularies Vocabularies Export Path Browse Vocabularies Directory Browse Max Steps to Simulate 50 Automaton to Simulate Restore Defaults Apply cme e The Debug check box turns on and off the debugging functionality 12 e The Start Mode option toggles how often the simulation will pause While in run mode the s
4. find gui tempo exe file This file can be executed either by double clicking or directly from the command prompt Macintosh OS X Using the Finder click on tempo app in the Tempo installation directory Alter natively from the command line in a terminal emulator cd to the Tempo installation directory and type open a tempo Linux Use the command line to cd to the Tempo installation directory Then type tempo The first time the UI is started a blank UI window will appear The window s appearance may vary slightly from platform to platform but will be similar to this lala File Edit Navigate Window Tools Help is J 100400Q0QUQ0Q I gt ALAE ES y Dz Outline 3 An outline is not available E Console 23 Problems Ex A ew Fog oTe Checker 3 3 Overview of the UI window By interacting with the UI users control both the contents and layout of the UI window A typical UI window looks like File Edit Navigate Window Tools Help lia 1 gt Ic61 0QQUIGIAQIDOALA A TS Navigator 23 S O 2 sample tioa x TE ERES Sautomaton Source ajm E My Specs gt signature 2 Sample tioa output send n Int internal increment states value Int 0 transitions output sendin pre n value internal increment eff value value 1 automaton Destination signature input send n Int states value Int 0 2 transitions input send
5. project directory will appear in the Navigator Now right click on the project directory in the Navigator and select New gt File to bring up the New File wizard Fill in a file name e g Sample tioa making sure that its name ends with tioa xi File Create a new file resource A Enter or select the parent folder My Specs DA W File name Sample tioa Advanced gt gt me Then click Finish In response the UI creates a new empty file opens an editor for that file and displays the file name in the Navigator Navigator X E My Specs Sample tioa 3 5 Writing and viewing Tempo specifications Now type a Tempo specification into the editor and observe how the UI highlights Tempo keywords o Sample tioa X automaton Source Signature output send n Int internal increment states value Int 0 transitions output sendin pre n value internal increment eff value value 1 automaton Destination Signature input sendin Int states value Int 0 transitions input sendin eff value n automaton A components S Source D Destination invariant of A S value gt D value EN The asterisk that appears next to the file name indicates that the editor has unsaved changes To save these changes either select File gt Save or use its shortcut Command S on a Macintosh Ctrl S elsewhere If the specificatio
6. signature output sendin Int internal increment states value Int 0 transitions output sendin pre n value internal increment eff value value 1 automaton Destination signature input send n Int states value Int 0 transitions input send n eff value n automaton A components S Source D Destination Transitions invariant of A S value gt D value i bo A send 3 increment pod Trajectories i 2 Tasks ag Destination as Signature 0 send int E ange i PVS translation stage completed Output path C CJ dev runtime tioaEditor product My Specs pvs Transitions 2 send poi Trajectories i ia 4 Tasks a A f 5 Components i he OS Each tool can be configured from the Tempo Preferences window located in Window gt Pref erences Preferences type filter text E General Install Update M El Tempo Plugins I validate Model Checker Ea PYS Simulator Some tools might provide additional output in the form of external files If the tool has generated additional output select Refresh from the projects context menu in the Navigator For example the PVS Translator tool generates an additional directory containing several output files 10 a Navigator X A_decls pws common_vocabs pys gt local strategies pws strategies gt x config 3 7 Sample tioa 4 Tempo Tools Tutorial
7. the current state of the UI e g the location of the cursor the progress of the current compilation Between the menu bar and the status bar are tabbed panes that contain editors and several kinds of views e The Navigator provides a hierarchical view of the projects collections of directories and files accessible to the UI e If a Tempo specification i e a file with a name ending in tioa appears in the currently active editor the Outline provides an overview of its contents vocabularies automaton definitions their primary components and assertions e The Problems view calls attention to errors detected by the Tempo parser and static semantic checker e The Console displays the textual output from the tools in the Tempo Toolset 3 4 Getting ready to write Tempo specifications Tempo specifications are stored in projects which are directories with some attached and generally hidden metadata To create a project right click in the Navigator and select New gt Project to bring up the first page of the New Project wizard Select a wizard lt gt Create a new project resource Wizards type filter text a Double click on the Project icon to bring up the second page of the wizard and enter a name e g My Specs for the new project New Project o Project Create a new project resource Project name My Specs cme Navigator X Then click Finish A new
8. A to PVS TAME translator User manual 2006 3 Sam Owre Sreeranga P Rajan John M Rushby Natarajan Shankar and Mandayam Srivas Pvs Combining specification proof checking and model checking In Rajeev Alur and Thomas A Hen zinger editors Computer Aided Verification CAV 96 volume 1102 of Lecture Notes in Computer Science pages 411 414 Springer Verlag 1996 VeroModo Inc TIOA Model Checker User Guide and Reference Manual 2006 VeroModo Inc The TIOA Simulator How To 2006 VeroModo Inc TIOA User Guide and Reference Manual 2006 CES D 15
9. The Tempo User Interface VeroModo Inc August 24 2011 Abstract The Tempo User Interface provides a convenient environment for developing and working with Tempo specifications It provides a Tempo aware editor automatic static checking and access to tools such as the Tempo simulator the Uppaal model checker the PVS theorem prover and the LaTeX translator This user interface is much easier to use than a standard text editor and the Tempo command line interface This document was prepared with version 0 2 4 Beta of the Tempo User Interface If you are using a newer version of the Ul some of the graphics in this document may be outdated Contents 1 2 Introduction 1 Recent Changes 1 Tutorial 1 3 1 Installing the Tempo Toolset ee 0 1 3 2 Starting the Tempo User Interface UI o 1 3 3 Overview of the Ul window 00600 a dd a OAK Loew ee ew 2 3 4 Getting ready to write Tempo specifications 2 0 a ee 3 3 5 Writing and viewing Tempo specifications 2 a eee eee 5 3 6 Checking specifications de a dd Be ee ai Foe te wht ho GA Ow 7 3 7 Checking multiple files together 00 a o A ae A ed A A 9 moo Usina Tempo Tools aia eh deere O EE A A 9 Tempo Tools Tutorial 11 io A IEEE 11 Ao Diet PE a y raa irc a A a da Be E 13 Implementation details 13 Troubleshooting 13 1 Introduction The Tempo User Interface the UI belongs to the Tempo Tools
10. This tutorial provides a brief introduction to special features of the Tempo Tools which are only available in the Tempo User Interface 4 1 Simulator In addition to the standard command line functionality the Tempo Simulator also supports a GUI driven debugger AE File Edit Navigate Window Tools Help Jti J5 2 J gt e OQeeRalPALFa Navigator A RETIE s cees O 2 Sample tioa 2 SimSample tioa Za 5 variable Name Value a E Ec CompositeAutomaton lt C gt Signature output foo compa BasicAutomaton lt 4 gt states dummy Int 74 dummy Int 74 transitions output foo compB BasicAutomaton lt B gt eff dummy dummy 2 dummy Int 75 automaton B signature input foo states dummy Int 75 transitions input foo eff dummy dummy 3 automaton C components compi compB B schedule r x fire output compa foo BE Outline 3 E gt O gt ha dummy Int al E e Transitions O Ro wf Trajectories E 1 i a Tasks El Console 23 Problems E ble ri co E E Signature ES r 3 foo Lo States Instantiate automaton B State variables for automaton C dummy Int id comp dummy 74 ei Pe S Transitions compB null i 2 foo Trajectories i a State variables for automaton C 4 Tasks C comp dummy 74 Components compB dummy 75 E O compa
11. e 3 Problems EXEC a e States Checker O value Int E ee Transitions al 2 send it a dD Components o 2 invariant of A 3 6 Checking specifications Static semantic checking is performed automatically on all Tempo specifications inside a project The editor indicates compilation errors by adding underlines and marks in the left margin Furthermore the Problems view lists all errors found in all open projects Console 2 ARTES 1 error O warnings O infos Hover over a marker in the left margin of an editor to see a description of the problem Double click on an error in the Problems view to highlight the error in an editor and to move the cursor there Description Resource Path Errors 1 item 3 undefined expression identifier something Sample tioa My Specs iix File Edit Navigate Window Tools Help lis J 10040Q0Q0QU0QQ I gt ALAE SS Navigator 3 H 2 Sample tioa 52 m Hi B z Sautomaton Source als a li My Specs 2 Sample tioa signature output sendin Int internal increment states value Int 0 gt transitions output sendin pre n value internal increment eff value value 1 automaton Destination signature input sendin Int states value Int 0 transitions input sendin ix eff value n something automaton A components S Source D Destination
12. et It provides a window based environment for writing Tempo specifications and for applying other tools to those specifications This manual provides a tutorial introduction to the UI It is not intended as an introduction to or reference guide for the Tempo Language 6 or the other tools in the Tempo Toolset the Tempo Simulator 5 and the interfaces to the Uppaal Model Checker 1 4 and the PVS Theorem Prover 13 2 Each of these tools has it s own user guide which can be found in the documentation directory of the Tempo Toolset 2 Recent Changes This document has been updated to version 0 2 4 Beta of the Tempo user interface All images have been updated and the content has been revised to reflect the latest version of the toolset 3 Tutorial This tutorial provides a step by step introduction to installing and using the Tempo User Interface 3 1 Installing the Tempo Toolset Visit http www veromodo com where the Tempo Toolset is available for download in the form of zipped bundles Download the bundle which best suits your system and unzip in the desired directory Tempo Toolkit is built on top of Java and we required either Java EE 1 5 or Java JDK 1 5 or later must be installed and configured prior to running this toolkit 3 2 Starting the Tempo User Interface UI Start the Tempo Ul by following the appropriate platform specific sequence of steps Windows Browse to the directory where the toolkit was unzipped and
13. imulator will run until it hits a break point and will pause at that break point While in step mode the simulator will pause at the first instruction 4 2 Other Plugins Currently the LaTex Uppaal and PVS translators do not have any extended functionality in the Tempo User Interface These tools can be configured via the Tempo preferences pages Details regarding usage of these configuration options can be found in each tool s respective user manual 5 Implementation details The UI stores the projects that it creates in the workspace subdirectory of the its installation directory The workspace subdirectory also contains a file netadata log 6 Troubleshooting Please report any problems to the Tempo development team This can be done by accessing the Tempo Ticket System look for it in the Links at http www veromodo com or directly via email support veromodo com Following are answers to the common problems After unzipping Tempo does not start On Mac and Linux systems this may be to the permission bits not set correctly 1 Mac OS open shell prompt and change directory to lt installationdirectory gt tempo osx xxx gui tempo app Contents MacOS then check if the execution bit is set using the following command 1s 1 tempo If the output you get is similar to rw r r 0 1 tempouser staff 25296 Aug 15 08 40 tempo then the execute bit is not set To fix it type in the following command chmod w tempo Now runni
14. n 8 eff value n something automaton A Pon components S Source D Destination B Outline SS te e E Transitions al invariant of A S value gt D value send gt increment t oft Trajectories E oa 0 a la 1 error O warnings O infos Description Resource Path Location E E Errors 1 item undefined expression identifier something Sample tioa My Specs line 17 2 send Int E do States ig 9 value Int 5 g Transitions o 2 send L Trajectories J Tasks A E dB Components os Lop 2 invariant of A y At the top of the UI window is a menu bar which contains six pull down menus on a Macintosh the six Tempo menus appear in the menu bar at the top of the desktop not in the UI window Three of these menus File Edit and Help provide standard functionality for text editors e g creating and saving files cutting and pasting text and obtaining help Another Navigate enables users to jump to a specified location in a file The Window menu enables users to control the appearance of the UI window and allows access to the Tempo Toolset prefrence pages The Tools menu provides access to the Tempo Toolset Below the menu bar is a toolbar which enables users to perform certain tasks quickly by clicking an icon At the bottom of the UI window is a status bar which provides useful information about
15. n contains no syntactic errors the Outline view will provide a hierarchical view of its contents Outline X Source B Signature send Int gt increment El de States value Int oe Transitions 2 send increment Trajectories Yi Tasks EJ Q Destination 3 Signature gt send Int de States O value Int e Transitions gt send Both the outline and the text being edited can be collapsed or expanded independently by clicking on the plus or minus signs in the boxes in the outline or in the circles in the left margin of the editor Selecting an item in the outline causes the editor to highlight the corresponding region of text File Edit Navigate Window Tools Help le la SS Navigator 3 JS OQBGBARGaI gt DHEAE 101 x O 2 Sample tioa 23 a Jl EZX Sautomaton Source a li My Specs F Sample tioa gt signature output send n Int internal increment states value Int 0 gt transitions output sendin pre n value internal increment eff value value 1 automaton Destination Signature input send n Int states value Int 0 transitions input sendin eff value n E a B F Sample tioa invariant of A S value gt D value HQ s ource Q Destination he E E Signature Ki o en El consol
16. ng ls 1 tempo should return something like this rwxr xr x 1 tempouser staff 25296 Aug 15 08 40 tempo 2 Linux distributions open shell prompt and change directory to lt installationdirectory gt tempo linux _xxbit gui then check if the execution bit is set using the following command ls 1 tempo If the output you get is similar to rw r r 1 tempouser staff 25296 Aug 15 08 40 tempo then the execute bit is not set To fix it type in the following command chmod 755 tempo Now running 1s 1 tempo should return something like this 13 rwxr xr x 1 tempouser staff 25296 Aug 15 08 40 tempo Tempo fails to start and I get a JVM error message On different systems behavior may differ but in general after attempting to run the toolkit a JVM error message appears or a general error message stating that the error was written to a log file The error will look something like this gt 1313413960474 log Desktop tempo L_32 gui configuration gedit d moren y save g a 1313413960474 log M ISESSION 2011 08 15 09 12 40 298 nn rene nnn nnn o eclipse buildId unknown java version 1 6 0 26 java vendor Sun Microsystems Inc BootLoader constants OS linux ARCH x86 WS gtk NL en US Command line arguments os Linux ws gtk arch x86 ENTRY org eclipse osgi 4 O 2011 08 15 09 12 40 861 IMESSAGE Application error ISTACK 1 java lang RuntimeException No application id has been found at org eclipse e
17. quinox internal app EclipseAppContainer startDefaultApp EclipseAppContainer java 242 at org eclipse equinox internal app MainApplicationLauncher run MainApplicationLauncher java 29 at org eclipse core runtime internal adaptor EclipseAppLauncher runApplication EclipseAppLauncher java 110 at org eclipse core runtime internal adaptor EclipseAppLauncher start EclipseAppLauncher java 79 at org eclipse core runtime adaptor EclipseStarter run EclipseStarter java 344 at org eclipse core runtime adaptor EclipseStarter run EclipseStarter java 179 at sun reflect NativeMethodAccessorImpl invoke0 Native Method at sun reflect NativeMethodAccessorImpl invoke NativeMethodAccessorImpl java 39 at sun reflect DelegatingMethodAccessorImpl invoke DelegatingMethodAccessorImpl java 25 at java lang reflect Method invoke Method java 597 at org eclipse equinox launcher Main invokeFramework Main java 622 at org eclipse equinox launcher Main basicRun Main java 577 at org eclipse equinox launcher Main run Main java 1410 Probably the cause of this message is architectural incompatibility of your JVM with the one used to build the distribution bundle To remedy this problem you must install the appropriate JVM or configure run options of the tempo file so that it is opened using the right version 14 References 11 K G Larsen P Pettersson and W Yi Uppaal in a nutshell Journal of Software Tools for Technology Transfer 1 2 134 152 1997 2 Hongping Lim TIO
18. ype Check Automatically gt signature output send n Int internal increment states value Int 0 gt transitions output sendin pre n value internal increment eff value value 1 automaton Destination signature input send n Int states value Int 0 gt transitions input send n eff value n maton A mponents S Source D Destination riant of A S value gt D value Ei P E console 23 N Problems Ge OE 4 Gro O Checker E My Specs The Check Automatically mode will check the specification each time it is saved The Check As You Type mode will check the specification as it is being typed into the editor The Clean option marks a file as out of date The file will be re checked the next time automated checking occurs If neither Check Automatically or Check As You Type are enabled the specification must be built manually e The Build Together option will be explained in the Checking multiple files together section of this tutorial 3 7 Checking multiple files together By default the Ul will analyze each tioa file separately In some cases it is convent to break one specification across several files A project can easily be configured to compile all if it s files together by right clicking the project and selecting Build Options gt Build Together
Download Pdf Manuals
Related Search