Add default graph options to toolbox TLC launcher and remove basic spec

org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/job/TLCJob.java

@@ -228,9 +228,10 @@ public abstract class TLCJob extends AbstractJob implements IModelConfigurationC
         final boolean visualizeStateGraph = launch.getLaunchConfiguration().getAttribute(LAUNCH_VISUALIZE_STATEGRAPH, false);
 		if (visualizeStateGraph && hasSpec) {
 			// Visualize state graph when requested and a behavior spec is given. A behavior
-			// spec is required for TLC to create states.
+			// spec is required for TLC to create states. Default to always colorize edges and 
+			// add action edge labels.
 			arguments.add("-dump");
-        	arguments.add("dot");
+			arguments.add("dot,colorize,actionlabels");
 			arguments.add(modelName);
 		}
       

tlatools/test-model/BasicModel/BasicSpec.tla

----------------------------- MODULE BasicSpec -----------------------------------
-EXTENDS Naturals, FiniteSets
-
-VARIABLE varA, varB
-Max == 3
-
-Init == varA = 0 /\ varB = 0
-
-IncA == (varA' = (varA+1) % Max) /\ UNCHANGED varB
-IncB == (varB' = (varB+1) % Max) /\ UNCHANGED varA
-IncAB == (varA' = (varA+1) % Max) /\ (varB' = (varB+1) % Max)
-
-Next == \/ IncA 
-        \/ IncB 
-        \/ IncAB
-
-================================================================================

tlatools/test-model/BasicModel/MC.cfg

-INIT
-init_mc
-NEXT
-next_mc
\ No newline at end of file

tlatools/test-model/BasicModel/MC.tla

----- MODULE MC ----
-EXTENDS BasicSpec, TLC
-init_mc == Init
-next_mc == Next
-=============================================================================
-\* Modification History
-\* Created Tue Feb 10 18:35:02 CET 2015 by markus