The LEADSTO/TTL Software Environment Users Manual

Contents

Introduction

Documentation

The separate "getting started" pdf documents introduce the tools:

Introduction to the Software

Leadsto Software
A graphical editor is available for creating leadsto specifications. It is called lteditor.

The leadsto simulation program may be used to perform the following operations:

Generate trace
Generate a trace from a loaded specification.
Load trace
Load a trace from an earlier session
Show trace
Show a trace in a graph.

There are two versions of the simulation program:

leadsto
A version with a more advanced GUI, allowing for loading/simulating/displaying multiple specifications
ltbare
A version which performs one operation controlled by command line options.
TTL Checker Software
The ttlchecker program is a combined graphical editor and checker for TTL-formulae. All programs have lots of command line options. Running
ltbare --help
or
leadsto --help
or
ttlchecker --help
will output information on command line options.

Installation

Currently the software is available for Windows, Linux (Redhat 7.1) and Solaris.

Installation Instructions for Windows

Install the leadsto software by running the setup executable install_leadsto.exe.

Working at the Vrije Universiteit on Windows

  1. Make sure you have a correctly mapped network drive T: pointing to \\tornado\practica.
  2. Make sure you have a correctly mapped network drive H: pointing to your UNIX home directory
  3. Make sure you don't mind if a directory ltwrk is created in your home directory.
  4. Double click on T:\AI\projects\setupltsim: This creates a directory ltwrk with an ltwrk/examples sub-directory. It also places shortcuts on your desktop.
  5. Double click on the
    • leadsto icon on the desktop to run a simulation,
    • ttlchecker icon on the desktop to create/edit or check TTL-formulae.

Instructions at the Vrije Universiteit on Solaris

Execute Run in a directory where you have write permission, as the program will create several log files.

If you add /usr/local/ai/lt/bin to your environment variable PATH, you may simply type lteditor, leadsto, ttlchecker. (How to do that depends on the Unix-shell you have (execute : echo $SHELL) and what environment file you normally put your environment variables in. For $SHELL = */bash: Edit your .bashrc or .bash_profile file: look for a line "export PATH= ..." and add :/usr/local/ai/lt/bin)

Installation Instructions for Linux

We do not update and test new versions of the Linux version of the software as we do the windows version.

  1. Download the file ltrhlinux71.tgz or another obviously linux installation tgz file.
  2. Install its contents somewhere conveniently:
      $ tar -zxf ltrhlinux71.tgz
    
  3. This will create a subdirectory lt/.
  4. Do not forget:
      $ cd lt/plrt/bin;./chplhd
    
  5. Run leadsto by executing lt/bin/leadsto. Other programs are available in the lt/bin/ directory. You should probably add lt/bin/ to your PATH environment variable.
The ltrhlinux71.tgz (old) software has been tested only on different installations of Redhat 7.1. There are other more recent/other version linux installations avalaible. Try the most recent ones first. (Please e-mail lourens@cs.vu.nl with your experiences with installing on Linux)

Known problems installing on Linux

One known problem is that you may get an error: undefined symbol rl_readline_state. You may try to upgrade your "readline" library to version 4.2. Otherwise you could try:
$ export LD_LIBRARY_PATH=your_install_dir/lt/lib:$LD_LIBRARY_PATH
$ your_install_dir/lt/bin/leadsto
This will load the readline library in the lt directory instead of the one in your linux installation. You could write a script that contains this setting of LD_LIBRARY_PATH.

Getting Started with the Leadsto editor (lteditor)

On Windows, double click the lteditor icon on your desktop. On unix, execute lteditor.

The white canvas will contain the tree representation of your specification. Initially there is one node, named ROOT. Manipulation of nodes is possible by right clicking with your mouse pointing to the node. All elements of your specification will be branches of this ROOT node.

Suppose you wish to specify that atom seed is true between times 0 and 10:

  1. Mouse over ROOT, click right mouse button; a menu will appear.
  2. While holding down the mouse button, point to the entry Interval. Release the mouse button. A subtree will appear, representing an interval rule.
  3. To fill in the range, click right mouse button on the node "R: range([time],[time])". Release the button when over edit. A window with name "Range Editor" will appear.
  4. Edit the line "range([time],[time])". Replace both times, i.e. result should be "range(0,10)". Press button Ok. In the canvas you will see the change.
  5. Next edit the entry representing the formula, marked F [formula] by placing the mouse over that text, right click and release over entry Change atom. The node will be changed into F [atom]
  6. Edit this atom by right mouse button click over F [atom], and release when over entry Edit. Change the value in the white text area into seed
  7. To save the specification entered, click on the second icon below the File entry (looks like a floppy) and specify a file name (without extension), say savedseed.
  8. To run the simulation at this stage, (leave the lteditor open), double click on the icon leadsto. A new window with header "Leads To Simulation Tool" will appear.
  9. To load the just saved file, click on the first icon below File (folder icon). A file chooser window will appear, select the file you saved two steps ago.
  10. Back to the editor: Suppose you wish the simulation to run from time 0 to time 50 (instead of the default time 200). You need to add a child node of kind end_time to ROOT.
    Right click on the interval node and release over insert above.
    A [specification_element] node will appear.
  11. Right click on this node and select end_time. Node changes into end_time([time])
  12. Edit end_time([time]) by right clicking and selecting the Edit entry. Change [time] into 50, press button Ok.
  13. You could save and run again as described about five steps before.
  14. Suppose you wish to add a rule seed o-->> tree with parameters e= 0, f = 0, g = 1, h = 1:
    Right click select insert below over interval node.
  15. Change new [specification_element] into Leadsto node.
  16. The Leadsto node has two children A:[formula] (A for antecedent) and C:[formula] (C for consequent).
    Change the A: node into an atom and edit it to change it into seed. (Due to a bug the A:, C: labeling may become confused).
  17. Change the C: node into an atom tree
  18. Add the parameters: Right click on the leadsto node and select add delay.
  19. Edit the EFGH: efgh([time],[time],[time],[time]) node (right click on it and select edit). Replace the [time] strings with our delays, i.e. the result should be efgh(0,0,10,30).
  20. Save the specification and reload it in the Simulation Maker
The saveseed example will look like

Missing Picture of Tree

Getting Started with the Checker (ttleditor/ttlchecker)

The checker software allows one to check whether a given ttl-formula is satisfied for a set of traces.

A separate editor for ttl-formula called ttleditoris available, but the ttl-formula checker ttlchecker itself allows you to create and check formula in one GUI.

  1. Be careful when checking a formula: lots of errors in your specification may lead to exiting the checker program. If you do not wish your editing work to get lost, save your ttl specification before checking.
  2. A trace is needed if you wish to check trace properties. The traces generated by leadsto may be loaded into the checker. If you wish to load different traces, after doing a simulation, rename the generated trace file trace.tr to some other file, such as sugarscape.tr
  3. Start up ttlchecker(by double clicking the shortcut on windows or executing ttlchecker on unix/linux).
  4. Edit properties and sorts functions in the same way as editing nodes in the leadsto editor described above.
  5. You may define sorts and properties in the ttlchecker/ttleditor.
  6. You may check a formula by right clicking on a property and selecting "Check property verbose" or "Check property quiet".
    This will compile the formula the property represents and will start checking. The "verbose" variant will give lots of output on the background window which may provide you with some information on why a ttl-formula is not satisfied.
    Only properties containing no variable arguments with all generic parts filled in may be checked.
  7. You may reuse sort definitions from your .lt specifications by copying such files into .fm files and reading them in. Unrecognised leadsto elements will then be ignored and when you save the loaded ttl-specification, only ttl-elements will remain.
  8. Loading traces:
    1. Select File => Trace Management...: a "Checker Trace Management" window should appear.
    2. Press the Add trace button: a File chooser window should appear.
    3. Select a trace file to add (double click, or open)
    4. If you do not like the default name, select the added trace name (trace1,trace2,..) and edit the Trace name: entry.
  9. The traces as generated by the leadsto software are "compacted", i.e. only distinct time intervals are used with integer values starting at 0. This means that you should not use absolute times as occurring in the leadsto specification in ttl-formulae. You may inspect the "compacted" trace by pressing the button "Save compacted traces" which will create files generated_compacted_trace_trace1.tr, generated_compacted_trace_trace2.tr etc. Reload these trace files into leadsto by selecting load in leadsto and changing Filter: into Trace in the file chooser window.
  10. For better error messaging, use var:sort everywhere in your formulae where you would use var.
  11. Take care that arithmetic expressions are recognised automatically. This implies that a(e, pi) will be interpreted as a(2.718.., 3.141..).

Specifying multiple traces in one specification

Getting started

  1. Load and inspect model1.lt (from the examples) into your lteditor.
    MODEL m1(D:between(10,12)) 
    
    introduces a constant D in the leadsto specification. Three traces will be produced for D=10,D=11,D=12. D may be used as a constant almost everywhere. Detection is not complete yet (probably not detected in sort definitions), if you miss some substitution, e-mail lourens please. In this example D is used as the delay parameter in a leadsto rule.
  2. Load model1.lt into leadsto. Traces will be generated and all traces are gathered in one trace file (defaulting to trace.tr).
    The implementation is incomplete in so far that you cannot inspect the different traces yet.
  3. Load model1.fm into ttlchecker. Next load the trace file (trace.tr) through the GUI: File->TraceManagement. As first trace you will now see m1(D:between(10,12)). But this is a set of traces. Sort TRACE will contain m1(10),m1(11), m1(12).

More details

By defining an entry model(modelname(Name1:Sort1,Name2:Sort2,..,NameN)) in your leadsto specification, constants Name1, Name2,.. NameN may be used in your leadsto specification. The value of NameI will be instantiated to an element in SortI. Th3e leadsto program will generate just as much traces as there are instantiations of Name1,..NameN. The name of a specific trace will be modelname(Value1,Value2,..ValueN).

There is no magical improvement in performance! Generating N traces still takes N times as much time as generating a single trace.

Example:

model(m1(Delay:between(10, 12))).
interval([], range(0, 1), a).
leadsto([], a, b, efgh(Delay, Delay, 1, 1)).
In trace m1(10) constant Delay will have value 10, in m1(11) constant Delay is 11.

Loading the trace file into a ttl specification will add objects/terms m1(10),m1(11),m1(12) to sort TRACE and have those three traces loaded.

Communication Visualisation

Most recent added features and explanations

introduction

Very experimental. After loading and running a simulation or after loading a trace the communication between roles may be visualised by a changing graph. Currently only atoms of the form output(From)|communication_from_to(From, To, T1, T2) are considered and the contents of T1 and T2 are ignored. In principle as soon as such an atom becomes true, a connection is made between two nodes named From and To.

Getting started

  1. Load and run a simulation or load a trace. You could start out with the highlevel2.lt example.
  2. Select File->Show Communication Graph
  3. A graph is shown containing all nodes and all occurring communications. The window will probably be too small to comfortably hold all nodes, so resize the "Communication Analysis Tool" window and in this window select File->Layout
  4. Next, optionally, move around nodes by left mouse button dragging them around, so that the node/links become more pleasing to the eye.
  5. If you wish to save that pleasing initial configuration, select File->Save As Initial Position. Later on you may reload this configuration by selecting Load Initial Position. For demonstration purposes you could try loading the highlevel2a.nl initial settings.
  6. Next, select File->Show communication..

Activities

  1. Arrows better visible if link becomes wider
  2. busy roles more intense
  3. Make constants more accessible
  4. Change colour and/or size of nodes when more involved with communication.
  5. Saving a communication visualisation run and rerunning it from saved state and allowing editing.
  6. Attract most recent, most busy nodes to center.
  7. Make nodes bigger when they have been more busy recently.
  8. SVG replay?
Finished:
  1. Make constants more accessible.
  2. Make nodes bigger when they have been more busy recently.
  3. Is a bug:the distance now has a maximum strength 1, and decays. This should be start out with one after comm , decay some, add one after next comm, etc.
  4. Keep all communication links in the visualisation.

Checker details

Countably infinite sorts

Sorts dealing with time will be dealt with in the next section.

Under certain restrictions you may use variables of countably infinite sorts in formulae. In existential quantifiers

         exists([..X:infinite_sort,..], Formula)
the first occurrence of X in Formula should be in a positive holds subformula. Any other occurrences, such as in comparisons should be after that first occurrence.

In universal quantifiers

         forall([..X:infinite_sort,..], Formula)
Formula must be an implication: Formula = implies(F1, F2) and first occurrence of X in F1 should be in a positive holds subformula.

The "first-occurrence-of-variable-in-positiveholds" of variable X in formula F says that if F is a conjunction of subformulae, that if there is a subformula where X occurs first (from left to right), it must be in a holds term. Within this subformula the same property should hold(recursively).

A subformula could also be an existential quantification. In that case if X occurs in the existential quantification sub formula, its first occurrence there should be in a positive holds subformula (recursively).

A subformula could also be a unification, consisting of a toplevel implication, i.e.

forall(... , implies(F1, F2))
Here if X occurs in implies(F1, F2) then the first occurrence of X in formula should be in a positive holds subformula of F1.

Any variable having the first-occurrence-in-positive-holds property will be much more efficiently coded. For infinite sorts the property must hold.

For the time being we do not allow the first-occurrence-in-positive-holds occurrence to be preceeded by a disjunction of which one branch binds X, but the other one does not.

Sorts dealing with time

The leadsto software associates sort REAL with the time axis.

The checker has as input a trace of holds facts that are true/false for finite REAL time intervals.

The checker does not allow using REALS as time parameters to test properties, as there are infinitely many times that a holds fact is true if there are any holds facts in the trace.

The checker analyses the formula and determines what holds facts are present in the formula. After that the checker determines what REAL time intervals occur in the trace. The intervals are made maximal, i.e. all consecutive intervals that have identical holds values are taken together.

This leads to a number of intervals NI. A builtin sort has a range between 0 and NI - 1. There are different names for this sort. The preferred one is "interval".

In formulae there are functions available for values of the lower and upper bounds:

begin(i:interval)
gives the REAL value of the starting time of the interval in the trace.
end(i:interval)
gives the REAL value of the end time of the interval in the trace.
last_interval
Sort interval ranges from 0 to (including) last_interval.
Another function is:
interval(T:REAL)
giving the interval in which time T is. The interval is defined as [begin,end)
time(i:interval)
In holds facts in the state argument times may be REAL values, integers or the special function time(i:interval). This function is only defined at the correct position in holds formulae.
In quantifiers it is always allowed to use variables of sort interval, as that is a finite sort. It is also allowed to use integers representing time in quantifiers if you take care that such integer time quantifier variables have the first-occurrence-in-positive-holds property as defined in the previous section. Example:
denotes(ep2s,
    forall([t:interval >= interval(24), e3:integer],
           implies(holds(state(trace1,time(t:interval)), 
                         day_used_energy(e3:integer),true),
		   e3:integer = 8
           )
          )
).

leadsto specifications/details

General aspects of leadsto specifications

There are two ways of producing a "leadsto specification":
  1. Use the graphical editor to produce a file.
  2. Using your own text editor, create a specification consisting of terms as described in section Allowed constructs
Even if you use the graphical editor, browse section Allowed constructs to get an impression of what constructs are available.

In case you prepare your own text file: The specification has a prolog-like syntax and is read from this file (the graphical editor writes such text files).
Major characteristics of this prolog syntax are:

The current software requires all atoms to be well-formed Prolog terms.

Allowed constructs

The specification may also contain Prolog code such as for sort definitions. (Not supported by the graphical editor).

Remark on alphabetical sorting

Alphabetical sorting is based on ordering of terms in the Prolog programming language: Terms with a lower number of arguments (irrespective of their name) have a lower order than terms with more arguments, so
z, y(a), y(b), a(b,c), b(a,a)
is sorted.

Sort definitions

For the time being there are two ways of defining sorts:
  1. Use sortdef, i.e. sortdef(<Sort-Name>, [<Ground-Term>,...]).
    as described above. This is the preferred way.
  2. sort_element(s(X), Y) :-
          member(Y, [f(X), g(X), h])
    
    leading to s(1 + 3) having elements f(4), g(4) and h. This allows more complex sort definitions. But the leadsto editor does not support such constructs.

Predefined sorts

REAL
Variables of type real. (If you specify this sort in your own text file, you should put single quotes around REAL)
INTEGER
Variables of type integer. (Same remark with regarding to quoting as for sort REAL )
between(I1, I2)
Variables of type integer constrained between two values I1 and I2, i.e. x: x >= I1 and x <= I2

Numerical expressions

Operators "+", "-", "*", "/", "mod", "exp" are handled in a special way: operands are either numbers or variables instantiated to numbers.
Limitation: for the time being the first occurrence of a variable that is present in the initial <:Vars> list should not be part of an operation.

Printing

For printout right click on the window and select one of the options. Option Print will print to an installed printer on windows or send to the printer on solaris at the VU (executes lpr -P $PRINTER tmpfile.ps).

Saving and later reproducing traces

A leadsto simulation session produces a file trace.tr which gets overwritten each simulation. If you wish to keep it, rename the trace.pl file. To inspect the trace, run leadsto -displaytrace TRACEFILE.

Remarks on the AGR model atom representation

If you wish the checker software to interpret traces generated with the leadsto software, the "|" prefix is reserved for expressing input/output/internal, role, relation tuples:
output(R:'ROLE')|relation(arg1,..)
input(R:'ROLE')|relation(arg1,..)
internal(R:'ROLE')|relation(arg1,..)
lead to holds relations in the ttl formulae:
holds(state(trace1, t1, output(R:'ROLE')), relation(arg1,..), trueorfalse)
holds(state(trace1, t1, input(R:'ROLE')), relation(arg1,..), trueorfalse)
holds(state(trace1, t1, internal(R:'ROLE')), relation(arg1,..), trueorfalse)
The checker software needs this syntax of defining role/input/output.

Remarks on use of variables

Interval rules will be instantiated completely. This implies that all sorts occurring at all places should have finite domains.

Variables may occur almost everywhere in leadsto rules and interval rules. If those variables obey certain requirements, they may even be of infinite sorts. These requirements will follow in the next paragraph. If these requirements are not met for some variable, the variables will be instantiated, leading to the generation of one rule per variable instantiation.

Leads to rules may contain variables of non finite domains. There are severe restrictions on the use of such variables:

  1. Infinite domain variables may not occur in delays: NOT ALLOWED
    leadsto([x:'INTEGER'], a(x), b(x), efgh(1, 1, x, x)).
    
  2. They may not have range restrictions: NOT ALLOWED
    leadsto([x:'INTEGER'< 10], a(x), b(x), efgh(0,0,1,1)).
    
  3. They may not occur as range variables in quantifiers inside formulae: NOT ALLOWED:
    leadsto([], forall([x:'INTEGER'],a(x))  , b, efgh(0,0,1,1)).
    
  4. They may not occur as arguments in rule parts such as sorts, constant part of conditions, etc. Only inside atoms in formulae. NOT ALLOWED:
    leadsto([x:'INTEGER'], forall([y:between(1,x)],a(y), b(x), efgh(1, 1, x, x)).
    
    leadsto([x:'INTEGER'], forall([y:between(1,3)< x + 2],a(y), b(x), 
    efgh(1, 1, x, x)).
    
  5. If an infinite domain variable occurs only in the antecedent, this is allowed, but may lead to warnings if multiple instantiations lead to the same result.
  6. Infinite domain variables may not occur only in the consequent.
Variables occurring in leadsto rules are split into two kinds: Global variables encompassing the whole leadsto rule, called global variables and local variables, i.e. variables defined in quantifiers inside the antecedent or consequent.

Local variables will be completely instantiated, internally transforming forall quantifiers into conjunctions.

Global variables are analysed for their occurrence in the body of the rule. If they occurs in places defined above as NOT ALLOWED, those variables will lead to instantiation as well, i.e. for each instantiation of those NOT ALLOWED variables, a rule is instantiated.

Restrictions on e, f, g, h

Details on working with real numbers

Before storing derived atoms, their real number arguments are rounded off, standard to about 7 digits long. There are facilities for more precise results. E-mail lourens@cs.vu.nl if you need more precise results.

Appendix

Trace syntax

Introduction

Traces need not be generated by the leadsto software. The checker expects trace files of a certain syntax. At the moment there are two formats for traces. One supports only one trace per file, called "single-trace" trace format, the other supports multiple traces per file, called "multi-trace" trace format. For the time being the "multi-trace" trace format cannot be shown by the leadsto software, but can be loaded into the checker.

General

Both format trace files must be correct prolog syntax. A.o. this implies:

Specific, common

Each trace may contain facts
content(SomeValue).
The checker recognizes and uses:
content(source(file(FileName, Parts)).
where parts is a prolog list, the checker only handles an entry path(Path) in the Parts list; if such an entry is present, it interprets that as filename of the generating source, otherwise it uses FileName.
content(run(RunData)).
where Rundata is a prolog list; the checker only recognises an entry date(Date) as the (modified/creation) date of the generating source file.

See the GUI for "trace management" in the checker for how the data is presented.

"single-trace" format

Example:
content(type(savedtrace('spec/simple.lt'))).
content(source(file('spec/simple.lt', [size(214), path('f:/cygwin/home/lourens/wrk/ww/db3/pl/spec/simple.lt')]))).
content(run([date('Thu Aug 19 10:43:03 2004')])).
atom_trace(tree, tree, [range(870.0, 1020.0, true), range(740.0, 870.0, false), range(590.0, 740.0, true), range(460.0, 590.0, false), range(310, 460.0, true), range(180, 310, false), range(30, 180, true), range(0, 30, false)]).
atom_trace(blossom, blossom, [range(960.0, 1110.0, true), range(830.0, 960.0, false), range(680.0, 830.0, true), range(550.0, 680.0, false), range(400.0, 550.0, true), range(270.0, 400.0, false), range(120.0, 270.0, true), range(0, 120.0, false)]).
atom_trace(seed, seed, [range(860.0, 1000, false), range(840.0, 860.0, true), range(580.0, 840.0, false), range(560.0, 580.0, true), range(300.0, 560.0, false), range(280, 300.0, true), range(20, 280, false), range(0, 20, true)]).
cwa(A).
times(0, 1000.0, 1000).
The atom_trace(AtomKey,Atom, Ranges) entries should speak for themselves apart from the first argument AtomKey. Later on you possibly will be allowed to leave out the argument, but for the time being you should add such an argument. The argument is the "quoted" version of the Atom argument.
If Atom is 'A'(p, 'Q') then AtomKey must be '\'A\'(p, \'Q\')'. The quoting becomes rather awkward. Best to look at example traces.

The entry times(StartTime,HandledTime,EndTime).: Just use HandledTime=EndTime. The times are the start and end times of a trace.

"multi-trace" format

The format is almost identical to the "single-trace" format. Each per trace entry gets an extra first argument representing the name of the trace. There is a separate entry trace(TraceName). for each trace.

There should be an entry model(Model, Size). in the file, where Size is the number of traces and Model represents the "generating term" for all trace names. (It is probably only used as an identification of the set of traces in the "trace management" of the checker.

Expected:

content(source(file('spec/model1.lt', [path('f:/cygwin/home/lourens/wrk/ww/db3/pl/spec/model1.lt']))).
content(run([date('Thu Aug 19 10:18:48 2004')])).
model(m1('D':between(10, 12)), 3).
trace(m1(10)).
atom_trace(m1(10), a, a, [range(1, 200, false), range(0, 1, true)]).
atom_trace(m1(10), b, b, [range(12, 200, unknown), range(11, 12, true), range(0, 11, unknown)]).
cwa(m1(10), a).
times(m1(10), 0, 210, 200).
trace(m1(11)).
atom_trace(m1(11), a, a, [range(1, 200, false), range(0, 1, true)]).
atom_trace(m1(11), b, b, [range(13, 200, unknown), range(12, 13, true), range(0, 12, unknown)]).
cwa(m1(11), a).
times(m1(11), 0, 205, 200).
trace(m1(12)).
atom_trace(m1(12), a, a, [range(1, 200, false), range(0, 1, true)]).
atom_trace(m1(12), b, b, [range(14, 200, unknown), range(13, 14, true), range(0, 13, unknown)]).
cwa(m1(12), a).
times(m1(12), 0, 209, 200).