ltbare --help

leadsto --help

ttlchecker --help

Installation

Installation Instructions for Windows

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

• /usr/local/ai/lt/bin/lteditor [leadstofile] to run a simulation (the argument is optional, but then the file must exist)
• /usr/local/ai/lt/bin/leadsto [leadstofile] to run a simulation
• /usr/local/ai/lt/bin/ttlchecker [fm-file] to create/edit or check ttl-formulae of a formula specification file. (The file argument is optional).

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

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.
   

Known problems installing on Linux

$ export LD_LIBRARY_PATH=your_install_dir/lt/lib:$LD_LIBRARY_PATH
$ your_install_dir/lt/bin/leadsto

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

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

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)).

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

• Remark: Once the communication visualisation window becomes visible, step or leap may be chosen. If commtrace ends, you need to press reset, to reset the state to the initial state/time. At the end of a trace step or leap simply do nothing. (Is a small bug).
• Beware: In Windows there is a bug in the handling of showing graphicals having the pen property > 1. So avoid that or at least do not do in on windows.
• Added a new program called commdemo1, in the solaris vu executable directory and Windows as a shortcut: it startsup leadsto and loads a graph comm demo.

• Suggestions for use

  Relating to demos

  1. First, you could copy the leadsto link and add a number of arguments. I often use (in Unix or cygwin:)

     leadsto -noshow -graphview g1 -graphinit spec/highlevel2a.nl -displaytrace highlevel2.tr
     

     -noshow suppresses the leadsto window(although the trace remains visible),
     -graphview g1 currently only results in showing the graph
     -graphinit FILE ensures that a previously saved initial situation is restored.
     -displaytrace File ensures that a certain trace will be loaded.
     

  2. Later on we may save settings with a trace. But for now, if you save the properties you set, they will be saved in a sub directory .xpce of your working directory in a file LeadsTo.cnf. You may perform different experiments in different directories and so have different stored settings.
• Made lots of graph alignment constants editable: Select Settings -> Properties.

  Some properties do not function yet. all Graph Sub Properties will have effect. There is a minimal amount of documentation with each property. <

  Some details:

  half time fraction

  Currently a global property that is a measure for how long one communication keeps a node or a communication link busy.

  Link Properties

  The width and length of a link is determined by the CommunicationStrength: sigma(commevent, 2^((Tcommevent-Tcurrent)/Half_time_fraction)) If CommunicationStrength >= MinimumLengthStrength then the ideal connection length is MinLength. If CommunicationStrength approaches 0 the ideallength will approach MaxLength. The link width will be UnitWidth*CommunicationLength. Two nodes will stop being attracted to each other as soon as the link width becomes 1.

  Node Properties

  The CommunicationStrength of nodes is defined by a similar expression, sum over all communications involving the node. For the time being the Diameter of a node is determined by DiameterProperty*(1 + CommunicationStrength*CommunicationFactor)

• Added buttons STEP, LEAP and RESET to the communication analysis window: Once a trace is loaded into the communication tool, you may activate all communications step by step one after another by repeatedly pressing STEP. If you wish to run through the rest of the communication, press LEAP. If you wish to go back to the intial communication situation, press RESET.
• In between steps you may move nodes and press File->Layout. The current layout will change and the run will proceed from the changed geometry; this has limited use as long as we cannot save runs.

introduction

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?

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

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

         exists([..X:infinite_sort,..], Formula)

In universal quantifiers

         forall([..X:infinite_sort,..], Formula)

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))

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 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.

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

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

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:

• Names starting with uppercase letters must be quoted.
• All syntactical constructs end with a full stop (".").
• All syntactical constructs are Prolog terms.

Allowed constructs

• constant(<Name-Term>, <Value-Term>).:
  Replace <Name-Term> by <Value-Term> wherever it occurs in the specification.
  Please do not use recursive replacements and do not use prolog variables here.
  Constants are currently not substituted in cwa, display*, model, start_time, end_time, global_lambda specification elements.
• start_time(<Time>).
  Simulation start time(default 0).
• end_time(<Time>).
  Simulation end time.
• interval(<Vars>,range(<Start-Time>, <End-Time>), <AndLiterals>).
  Make literals true in range <Start-Time> - <End-Time> for all instances of <Vars>, for example

  interval([x:between(1,10), y:between(1,10)<x],0, 10, and(f(x,y),not(g(x,x)))).
  

  Remarks:

  • Note that we used a sort between(1,10) here. So sorts may have parameters. between(L:INTEGER,H:INTEGER)

  • This is the preferred notation. It is allowed to define one constant for the <Range> argument, or even use a variable, as long as it simplifies/instantiates to range(<Start-Time>, <End-Time>)
  • The variables occurring in <Vars> may occur anywhere in the rest of the interval specification.
• interval(<Vars>, <Start-Time>, <End-Time>, <AndLiterals>).
  Same as above.
• interval( <Start-Time>,<End-Time>, <AndLiterals>).
  Same as above but no variables.
• periodic(<Vars>, range(<Start-Time>, <End-Time>),<Period-Time>,<AndLiterals>).
• periodic(<Vars>, <Start-Time>, <End-Time>,<Period-Time>,<AndLiterals>).
  In the graphical editor the only distinction between a periodic and non-periodic interval is that a period node is present or not.
• cwa(<VarAtom>).
  Is still incomplete, should contain variable specification, for now use prolog variables to specify a pattern for CWA atoms.
• global_lambda(<Factor>).
• leadsto(<Global-Vars>, <LHS-Formula>, <RHS-Formula>, <Delay>).
  where
  • <Formula> : not(<Formula>) | and(<Formula>[,<Formula>,...]) | forall(<Local-Vars>, <Formula>)
  • <Delay> : efgh(<E-Time>,<F-Time>,<G-Time>,<H-Time>) | unit
  
  Remarks:
  • The forall(<Local-Vars>, <Formula>) construct will be completely instantiated and replaced by an and construct.
  • If the <Local-Vars> construct refers to a variable in <Global-Vars> then these global-variables will also lead to partially instantiated rules.
  • <Global-Vars> says that there is a rule for each instantiation of <Global-Vars>.
  • All variables in <Global-Vars> should preferably occur in <LHS-Formula> as well as in <RHS-Formula>.
  • Disjunction and existential quantification are not yet supported.
• leadsto(<Formula>, <Formula>, <Delay>).
  same as above, but no global variables.
• sortdef(<Sort-Name>, [<Ground-Term>,...]).
  (where the [ and ] are list delimiters, not optional grammar meta info):Define sort as list of elements (sort name and objects may contain arguments, but for the time being they better not contain variables.
• display_number_range(<VarAtom>,<PrologVar>, <Relation-Tag-Name>, <Variable-Tag-Name>)
  if you wish to display a set of atoms that have a common numerical argument in 1 graph. See the specification examples/test/expfn.lt. The first versions of the leadsto editor will not support display_number_range.
• Display control
  Entries of the form display(ViewTag,Data) control what to show how. ViewTag is a tag that determines what view is active. It may be controlled by the commandline option -view ViewTag.
  • display(ViewTag, show_atoms(SomeAtom))
    If at least one such entry is present, only show those atoms matching SomeAtom. More than one entry "show_atoms(SomeAtom)" are allowed. The order in which the atoms are shown is the order that the "show_atoms(SomeAtom)" occur in the specification file. All atoms within one "show_atoms(SomeAtom)" will be sorted(see remark on alphabetical sorting). Take care: multiple "show_atoms(SomeAtom)" matching one atom will lead to multiple displays of this atom.
  • display(ViewTag, no_show_atoms(SomeAtom))
    Do not show atoms matching SomeAtom.
  • display(ViewTag,sort_atoms_global)
    Do not follow the order described for "show_atoms(SomeAtom)", but sort all atoms "globally"(see remark on alphabetical sorting).
  • display(ViewTag,sort_atoms_time_global)
    Sort all atoms in the trace according to their time of first occurrence in the trace with a truth value other than their default value(=unknown or false if cwa).
  • display(ViewTag,sort_atoms_time_abc_global)
    Sort all atoms in the trace according to their time of first occurrence in the trace with a truth value other than their default value(=unknown or false if cwa), sort atom names alphabetically for same times(see remark on alphabetical sorting).
  • display(ViewTag,sort_atoms_time)
    Sort atoms within each set of display(ViewTag, show_atoms(SomeAtom)) internally in time order as defined in display(ViewTag,sort_atoms_time_global).

Remark on alphabetical sorting

z, y(a), y(b), a(b,c), b(a,a)

Sort definitions

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

Printing

Saving and later reproducing traces

Remarks on the AGR model atom representation

output(R:'ROLE')|relation(arg1,..)
input(R:'ROLE')|relation(arg1,..)
internal(R:'ROLE')|relation(arg1,..)

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)

Remarks on use of variables

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.

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.

• leadsto([x:between(1, 1000)], a(x), b(x+1), efgh(0,0,1,1)).
  

  will not be instantiated and will have good performance.

• leadsto([x:between(1, 1000), y:between(x,x+1)], a(x), b(x), efgh(0,0,1,1)).
  

  will instantiate into 1000 rules.

• leadsto([x:between(1, 3), y:between(x,1000)], a(x,y), b(y+1), efgh(0,0,1,1)).
  

  is ok: x will be instantiated, but y will not.

Restrictions on e, f, g, h

• f > e is not allowed; this should lead to a warning and the rule should be ignored. Software versions up to version 0.91 did not check this requirement and could have produced incorrect results.
• Delays must all be numbers >= 0, not all 0, if H = 0 then G must be 0. An error message will be shown:

  ***ERROR:Delays must all be numbers >= 0, not all 0, if H = 0 then G must be 0, GOT efgh(0, 0, 0, 0)
  
  WARNING:Leadsto rule or interval has no instances
  

• If e,f = 0,0 g must be > 0 (for the time being), otherwise the simulation may produce an error:

  FATAL ERROR:No progress, probably used too much 0 time parameters...
  

Details on working with real numbers

Appendix

Trace syntax

Introduction

General

• Each entry must be a prolog term followed by a single dot.
• If a (leadsto/checker) atom contains an upper-case name, the name should be single quoted, so A(p,R) must be written as 'A'(p,'R').

Specific, common

content(SomeValue).

content(source(file(FileName, Parts)).

content(run(RunData)).

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

"single-trace" format

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 entry times(StartTime,HandledTime,EndTime).: Just use HandledTime=EndTime. The times are the start and end times of a trace.

"multi-trace" format

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).