Appended CONFIG in tla file will generate tla.dot file when dumping dot with ${modelName}.dot #483
Description
TLC Commands:
Without dumping Graphviz DOT file
-coverage 1 -cleanup -continue
With dumping Graphviz DOT file with model name: Issue is that the DOT file is named HourClock.tla.dot instead of HourClock.dot
-coverage 1 -dump dot,colorize,actionlabels ${modelName}.dot -cleanup -continue
----- MODULE HourClock -----
EXTENDS Naturals
VARIABLE hr
HCini == hr \in (1 .. 12)
HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1
HC == HCini /\ [][HCnxt]_hr
------------------------
THEOREM HC => []HCini
=======================
----- CONFIG HourClock -----
(***************************************************************************)
(* This is a TLC configuration file for testing that HCini is an invariant *)
(* of the specification HC *)
(***************************************************************************)
SPECIFICATION HC
\* This statement tells TLC that HC is the specification that it
\* should check.
INVARIANT HCini
\* This statement tells TLC to check that formula HCini is an
\* invariant of the specification--in other words, that the
\* specification implies []HCini.
======================Thanks and best regards,
Chris (zitro)