From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Concurrency/YieldTypeChecker.cs | 731 +++++++++++++++++---------------- 1 file changed, 368 insertions(+), 363 deletions(-) (limited to 'Source/Concurrency/YieldTypeChecker.cs') diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 95884626..ed59d3ad 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -1,363 +1,368 @@ -using System; -using System.Collections; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Boogie; -using System.Diagnostics.Contracts; -using Microsoft.Boogie.AbstractInterpretation; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics; - -namespace Microsoft.Boogie -{ - class YieldTypeChecker - { - static List> ASpec; - static List> BSpec; - static List> CSpec; - static YieldTypeChecker() - { - // initial: 0, final: 1 - ASpec = new List>(); - ASpec.Add(new Tuple(0, 'Y', 1)); - ASpec.Add(new Tuple(1, 'Y', 1)); - ASpec.Add(new Tuple(1, 'B', 1)); - ASpec.Add(new Tuple(1, 'R', 1)); - ASpec.Add(new Tuple(1, 'L', 1)); - ASpec.Add(new Tuple(1, 'A', 1)); - ASpec.Add(new Tuple(0, 'P', 0)); - ASpec.Add(new Tuple(1, 'P', 1)); - - // initial: 1, final: 0 - BSpec = new List>(); - BSpec.Add(new Tuple(1, 'Y', 0)); - BSpec.Add(new Tuple(1, 'Y', 1)); - BSpec.Add(new Tuple(1, 'B', 1)); - BSpec.Add(new Tuple(1, 'R', 1)); - BSpec.Add(new Tuple(1, 'L', 1)); - BSpec.Add(new Tuple(1, 'A', 1)); - BSpec.Add(new Tuple(0, 'P', 0)); - BSpec.Add(new Tuple(1, 'P', 1)); - - // initial: {0, 1}, final: {0, 1} - CSpec = new List>(); - CSpec.Add(new Tuple(0, 'B', 0)); - CSpec.Add(new Tuple(0, 'R', 0)); - CSpec.Add(new Tuple(0, 'Y', 0)); - CSpec.Add(new Tuple(0, 'B', 1)); - CSpec.Add(new Tuple(0, 'R', 1)); - CSpec.Add(new Tuple(0, 'L', 1)); - CSpec.Add(new Tuple(0, 'A', 1)); - CSpec.Add(new Tuple(1, 'B', 1)); - CSpec.Add(new Tuple(1, 'L', 1)); - CSpec.Add(new Tuple(1, 'Y', 0)); - CSpec.Add(new Tuple(0, 'P', 0)); - CSpec.Add(new Tuple(1, 'P', 1)); - } - - private void IsYieldTypeSafe() - { - List> implEdges = new List>(); - foreach (Tuple e in edgeLabels.Keys) - { - implEdges.Add(new Tuple(e.Item1, edgeLabels[e], e.Item2)); - } - //Console.WriteLine(PrintGraph(impl, implEdges, initialState, finalStates)); - ASpecCheck(implEdges); - BSpecCheck(implEdges); - CSpecCheck(implEdges); - } - - private void ASpecCheck(List> implEdges) - { - Dictionary> initialConstraints = new Dictionary>(); - initialConstraints[initialState] = new HashSet(new int[] { 0 }); - foreach (var finalState in finalStates) - { - initialConstraints[finalState] = new HashSet(new int[] { 1 }); - } - SimulationRelation x = new SimulationRelation(implEdges, ASpec, initialConstraints); - Dictionary> simulationRelation = x.ComputeSimulationRelation(); - if (simulationRelation[initialState].Count == 0) - { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum)); - } - } - - private void BSpecCheck(List> implEdges) - { - Dictionary> initialConstraints = new Dictionary>(); - initialConstraints[initialState] = new HashSet(new int[] { 1 }); - foreach (var finalState in finalStates) - { - initialConstraints[finalState] = new HashSet(new int[] { 0 }); - } - SimulationRelation x = new SimulationRelation(implEdges, BSpec, initialConstraints); - Dictionary> simulationRelation = x.ComputeSimulationRelation(); - if (simulationRelation[initialState].Count == 0) - { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum)); - } - } - - private void CSpecCheck(List> implEdges) - { - Dictionary> initialConstraints = new Dictionary>(); - foreach (Block block in loopHeaders) - { - if (!IsTerminatingLoopHeader(block)) - { - initialConstraints[absyToNode[block]] = new HashSet(new int[] { 0 }); - } - } - SimulationRelation x = new SimulationRelation(implEdges, CSpec, initialConstraints); - Dictionary> simulationRelation = x.ComputeSimulationRelation(); - if (simulationRelation[initialState].Count == 0) - { - moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum)); - } - } - - private bool IsTerminatingLoopHeader(Block block) - { - foreach (Cmd cmd in block.Cmds) - { - AssertCmd assertCmd = cmd as AssertCmd; - if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum)) - { - return true; - } - } - return false; - } - - public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker) - { - foreach (var impl in moverTypeChecker.program.Implementations) - { - if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue; - impl.PruneUnreachableBlocks(); - Graph implGraph = Program.GraphFromImpl(impl); - implGraph.ComputeLoops(); - int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; - foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum })) - { - if (layerNum > specLayerNum) continue; - YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers); - } - } - } - - int stateCounter; - MoverTypeChecker moverTypeChecker; - Implementation impl; - int currLayerNum; - Dictionary absyToNode; - Dictionary nodeToAbsy; - int initialState; - HashSet finalStates; - Dictionary, int> edgeLabels; - IEnumerable loopHeaders; - - private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable loopHeaders) - { - this.moverTypeChecker = moverTypeChecker; - this.impl = impl; - this.currLayerNum = currLayerNum; - this.loopHeaders = loopHeaders; - this.stateCounter = 0; - this.absyToNode = new Dictionary(); - this.initialState = 0; - this.finalStates = new HashSet(); - this.edgeLabels = new Dictionary, int>(); - - foreach (Block block in impl.Blocks) - { - absyToNode[block] = stateCounter; - stateCounter++; - foreach (Cmd cmd in block.Cmds) - { - absyToNode[cmd] = stateCounter; - stateCounter++; - } - absyToNode[block.TransferCmd] = stateCounter; - stateCounter++; - if (block.TransferCmd is ReturnCmd) - { - finalStates.Add(absyToNode[block.TransferCmd]); - } - } - foreach (Block block in impl.Blocks) - { - Absy blockEntry = block.Cmds.Count == 0 ? (Absy)block.TransferCmd : (Absy)block.Cmds[0]; - edgeLabels[new Tuple(absyToNode[block], absyToNode[blockEntry])] = 'P'; - - GotoCmd gotoCmd = block.TransferCmd as GotoCmd; - if (gotoCmd == null) continue; - foreach (Block successor in gotoCmd.labelTargets) - { - edgeLabels[new Tuple(absyToNode[gotoCmd], absyToNode[successor])] = 'P'; - } - } - - this.nodeToAbsy = new Dictionary(); - foreach (KeyValuePair state in absyToNode) - { - this.nodeToAbsy[state.Value] = state.Key; - } - - ComputeGraph(); - IsYieldTypeSafe(); - } - - private void ComputeGraph() - { - foreach (Block block in impl.Blocks) - { - for (int i = 0; i < block.Cmds.Count; i++) - { - Cmd cmd = block.Cmds[i]; - int curr = absyToNode[cmd]; - int next = (i + 1 == block.Cmds.Count) ? absyToNode[block.TransferCmd] : absyToNode[block.Cmds[i + 1]]; - Tuple edge = new Tuple(curr, next); - if (cmd is CallCmd) - { - CallCmd callCmd = cmd as CallCmd; - if (callCmd.IsAsync) - { - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; - if (currLayerNum <= actionInfo.createdAtLayerNum) - edgeLabels[edge] = 'L'; - else - edgeLabels[edge] = 'B'; - } - else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc)) - { - edgeLabels[edge] = 'P'; - } - else - { - MoverType moverType; - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; - if (actionInfo.createdAtLayerNum >= currLayerNum) - { - moverType = MoverType.Top; - } - else - { - AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; - if (atomicActionInfo == null) - moverType = MoverType.Both; - else - moverType = atomicActionInfo.moverType; - } - switch (moverType) - { - case MoverType.Atomic: - edgeLabels[edge] = 'A'; - break; - case MoverType.Both: - edgeLabels[edge] = 'B'; - break; - case MoverType.Left: - edgeLabels[edge] = 'L'; - break; - case MoverType.Right: - edgeLabels[edge] = 'R'; - break; - case MoverType.Top: - edgeLabels[edge] = 'Y'; - break; - } - } - } - else if (cmd is ParCallCmd) - { - ParCallCmd parCallCmd = cmd as ParCallCmd; - bool isYield = false; - bool isRightMover = true; - bool isLeftMover = true; - foreach (CallCmd callCmd in parCallCmd.CallCmds) - { - if (moverTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum) - { - isYield = true; - } - } - if (isYield) - { - edgeLabels[edge] = 'Y'; - } - else - { - foreach (CallCmd callCmd in parCallCmd.CallCmds) - { - ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc]; - isRightMover = isRightMover && actionInfo.IsRightMover; - isLeftMover = isLeftMover && actionInfo.IsLeftMover; - } - if (isLeftMover && isRightMover) - { - edgeLabels[edge] = 'B'; - } - else if (isLeftMover) - { - edgeLabels[edge] = 'L'; - } - else if (isRightMover) - { - edgeLabels[edge] = 'R'; - } - else - { - Debug.Assert(parCallCmd.CallCmds.Count == 1); - edgeLabels[edge] = 'A'; - } - } - } - else if (cmd is YieldCmd) - { - edgeLabels[edge] = 'Y'; - } - else - { - edgeLabels[edge] = 'P'; - } - } - } - } - - private static string PrintGraph(Implementation impl, List> edges, int initialState, HashSet finalStates) - { - var s = new StringBuilder(); - s.AppendLine("\nImplementation " + impl.Proc.Name + " digraph G {"); - foreach (var e in edges) - { - string label = "P"; - switch (e.Item2) - { - case 'P': label = "P"; break; - case 'Y': label = "Y"; break; - case 'B': label = "B"; break; - case 'R': label = "R"; break; - case 'L': label = "L"; break; - case 'A': label = "A"; break; - default: Debug.Assert(false); break; - } - s.AppendLine(" \"" + e.Item1.ToString() + "\" -- " + label + " --> " + " \"" + e.Item3.ToString() + "\";"); - } - s.AppendLine("}"); - s.AppendLine("Initial state: " + initialState); - s.Append("Final states: "); - bool first = true; - foreach (int finalState in finalStates) - { - s.Append((first ? "" : ", ") + finalState); - first = false; - } - s.AppendLine(); - return s.ToString(); - } - } -} +using System; +using System.Collections; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using Microsoft.Boogie; +using System.Diagnostics.Contracts; +using Microsoft.Boogie.AbstractInterpretation; +using Microsoft.Boogie.GraphUtil; +using System.Diagnostics; + +namespace Microsoft.Boogie +{ + class YieldTypeChecker + { + static List> ASpec; + static List> BSpec; + static List> CSpec; + static YieldTypeChecker() + { + // initial: 0, final: 1 + ASpec = new List>(); + ASpec.Add(new Tuple(0, 'Y', 1)); + ASpec.Add(new Tuple(1, 'Y', 1)); + ASpec.Add(new Tuple(1, 'B', 1)); + ASpec.Add(new Tuple(1, 'R', 1)); + ASpec.Add(new Tuple(1, 'L', 1)); + ASpec.Add(new Tuple(1, 'A', 1)); + ASpec.Add(new Tuple(0, 'P', 0)); + ASpec.Add(new Tuple(1, 'P', 1)); + + // initial: 1, final: 0 + BSpec = new List>(); + BSpec.Add(new Tuple(1, 'Y', 0)); + BSpec.Add(new Tuple(1, 'Y', 1)); + BSpec.Add(new Tuple(1, 'B', 1)); + BSpec.Add(new Tuple(1, 'R', 1)); + BSpec.Add(new Tuple(1, 'L', 1)); + BSpec.Add(new Tuple(1, 'A', 1)); + BSpec.Add(new Tuple(0, 'P', 0)); + BSpec.Add(new Tuple(1, 'P', 1)); + + // initial: {0, 1}, final: {0, 1} + CSpec = new List>(); + CSpec.Add(new Tuple(0, 'B', 0)); + CSpec.Add(new Tuple(0, 'R', 0)); + CSpec.Add(new Tuple(0, 'Y', 0)); + CSpec.Add(new Tuple(0, 'B', 1)); + CSpec.Add(new Tuple(0, 'R', 1)); + CSpec.Add(new Tuple(0, 'L', 1)); + CSpec.Add(new Tuple(0, 'A', 1)); + CSpec.Add(new Tuple(1, 'B', 1)); + CSpec.Add(new Tuple(1, 'L', 1)); + CSpec.Add(new Tuple(1, 'Y', 0)); + CSpec.Add(new Tuple(0, 'P', 0)); + CSpec.Add(new Tuple(1, 'P', 1)); + } + + private void IsYieldTypeSafe() + { + List> implEdges = new List>(); + foreach (Tuple e in edgeLabels.Keys) + { + implEdges.Add(new Tuple(e.Item1, edgeLabels[e], e.Item2)); + } + //Console.WriteLine(PrintGraph(impl, implEdges, initialState, finalStates)); + ASpecCheck(implEdges); + BSpecCheck(implEdges); + CSpecCheck(implEdges); + } + + private void ASpecCheck(List> implEdges) + { + Dictionary> initialConstraints = new Dictionary>(); + initialConstraints[initialState] = new HashSet(new int[] { 0 }); + foreach (var finalState in finalStates) + { + initialConstraints[finalState] = new HashSet(new int[] { 1 }); + } + SimulationRelation x = new SimulationRelation(implEdges, ASpec, initialConstraints); + Dictionary> simulationRelation = x.ComputeSimulationRelation(); + if (simulationRelation[initialState].Count == 0) + { + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum)); + } + } + + private void BSpecCheck(List> implEdges) + { + Dictionary> initialConstraints = new Dictionary>(); + initialConstraints[initialState] = new HashSet(new int[] { 1 }); + foreach (var finalState in finalStates) + { + initialConstraints[finalState] = new HashSet(new int[] { 0 }); + } + SimulationRelation x = new SimulationRelation(implEdges, BSpec, initialConstraints); + Dictionary> simulationRelation = x.ComputeSimulationRelation(); + if (simulationRelation[initialState].Count == 0) + { + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum)); + } + } + + private void CSpecCheck(List> implEdges) + { + Dictionary> initialConstraints = new Dictionary>(); + foreach (Block block in loopHeaders) + { + if (!IsTerminatingLoopHeader(block)) + { + initialConstraints[absyToNode[block]] = new HashSet(new int[] { 0 }); + } + } + SimulationRelation x = new SimulationRelation(implEdges, CSpec, initialConstraints); + Dictionary> simulationRelation = x.ComputeSimulationRelation(); + if (simulationRelation[initialState].Count == 0) + { + civlTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum)); + } + } + + private bool IsTerminatingLoopHeader(Block block) + { + foreach (Cmd cmd in block.Cmds) + { + AssertCmd assertCmd = cmd as AssertCmd; + if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && civlTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum)) + { + return true; + } + } + return false; + } + + public static void PerformYieldSafeCheck(CivlTypeChecker civlTypeChecker) + { + foreach (var impl in civlTypeChecker.program.Implementations) + { + if (!civlTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue; + impl.PruneUnreachableBlocks(); + Graph implGraph = Program.GraphFromImpl(impl); + implGraph.ComputeLoops(); + int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; + foreach (int layerNum in civlTypeChecker.AllLayerNums) + { + if (layerNum > specLayerNum) continue; + YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers); + } + } + } + + int stateCounter; + CivlTypeChecker civlTypeChecker; + Implementation impl; + int currLayerNum; + Dictionary absyToNode; + Dictionary nodeToAbsy; + int initialState; + HashSet finalStates; + Dictionary, int> edgeLabels; + IEnumerable loopHeaders; + + private YieldTypeChecker(CivlTypeChecker civlTypeChecker, Implementation impl, int currLayerNum, IEnumerable loopHeaders) + { + this.civlTypeChecker = civlTypeChecker; + this.impl = impl; + this.currLayerNum = currLayerNum; + this.loopHeaders = loopHeaders; + this.stateCounter = 0; + this.absyToNode = new Dictionary(); + this.initialState = 0; + this.finalStates = new HashSet(); + this.edgeLabels = new Dictionary, int>(); + + foreach (Block block in impl.Blocks) + { + absyToNode[block] = stateCounter; + stateCounter++; + foreach (Cmd cmd in block.Cmds) + { + absyToNode[cmd] = stateCounter; + stateCounter++; + } + absyToNode[block.TransferCmd] = stateCounter; + stateCounter++; + if (block.TransferCmd is ReturnCmd) + { + finalStates.Add(absyToNode[block.TransferCmd]); + } + } + foreach (Block block in impl.Blocks) + { + Absy blockEntry = block.Cmds.Count == 0 ? (Absy)block.TransferCmd : (Absy)block.Cmds[0]; + edgeLabels[new Tuple(absyToNode[block], absyToNode[blockEntry])] = 'P'; + + GotoCmd gotoCmd = block.TransferCmd as GotoCmd; + if (gotoCmd == null) continue; + foreach (Block successor in gotoCmd.labelTargets) + { + edgeLabels[new Tuple(absyToNode[gotoCmd], absyToNode[successor])] = 'P'; + } + } + + this.nodeToAbsy = new Dictionary(); + foreach (KeyValuePair state in absyToNode) + { + this.nodeToAbsy[state.Value] = state.Key; + } + + ComputeGraph(); + IsYieldTypeSafe(); + } + + private void ComputeGraph() + { + foreach (Block block in impl.Blocks) + { + for (int i = 0; i < block.Cmds.Count; i++) + { + Cmd cmd = block.Cmds[i]; + int curr = absyToNode[cmd]; + int next = (i + 1 == block.Cmds.Count) ? absyToNode[block.TransferCmd] : absyToNode[block.Cmds[i + 1]]; + Tuple edge = new Tuple(curr, next); + if (cmd is CallCmd) + { + CallCmd callCmd = cmd as CallCmd; + if (callCmd.IsAsync) + { + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; + if (currLayerNum <= actionInfo.createdAtLayerNum) + edgeLabels[edge] = 'L'; + else + edgeLabels[edge] = 'B'; + } + else if (!civlTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc)) + { + edgeLabels[edge] = 'P'; + } + else + { + MoverType moverType; + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; + if (actionInfo.createdAtLayerNum >= currLayerNum) + { + moverType = MoverType.Top; + } + else + { + AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; + if (atomicActionInfo == null) + moverType = MoverType.Both; + else + moverType = atomicActionInfo.moverType; + } + switch (moverType) + { + case MoverType.Atomic: + edgeLabels[edge] = 'A'; + break; + case MoverType.Both: + edgeLabels[edge] = 'B'; + break; + case MoverType.Left: + edgeLabels[edge] = 'L'; + break; + case MoverType.Right: + edgeLabels[edge] = 'R'; + break; + case MoverType.Top: + edgeLabels[edge] = 'Y'; + break; + } + } + } + else if (cmd is ParCallCmd) + { + ParCallCmd parCallCmd = cmd as ParCallCmd; + bool isYield = false; + bool isRightMover = true; + bool isLeftMover = true; + foreach (CallCmd callCmd in parCallCmd.CallCmds) + { + if (civlTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum) + { + isYield = true; + } + } + if (isYield) + { + edgeLabels[edge] = 'Y'; + } + else + { + int numAtomicActions = 0; + foreach (CallCmd callCmd in parCallCmd.CallCmds) + { + ActionInfo actionInfo = civlTypeChecker.procToActionInfo[callCmd.Proc]; + isRightMover = isRightMover && actionInfo.IsRightMover; + isLeftMover = isLeftMover && actionInfo.IsLeftMover; + if (actionInfo is AtomicActionInfo) + { + numAtomicActions++; + } + } + if (isLeftMover && isRightMover) + { + edgeLabels[edge] = 'B'; + } + else if (isLeftMover) + { + edgeLabels[edge] = 'L'; + } + else if (isRightMover) + { + edgeLabels[edge] = 'R'; + } + else + { + Debug.Assert(numAtomicActions == 1); + edgeLabels[edge] = 'A'; + } + } + } + else if (cmd is YieldCmd) + { + edgeLabels[edge] = 'Y'; + } + else + { + edgeLabels[edge] = 'P'; + } + } + } + } + + private static string PrintGraph(Implementation impl, List> edges, int initialState, HashSet finalStates) + { + var s = new StringBuilder(); + s.AppendLine("\nImplementation " + impl.Proc.Name + " digraph G {"); + foreach (var e in edges) + { + string label = "P"; + switch (e.Item2) + { + case 'P': label = "P"; break; + case 'Y': label = "Y"; break; + case 'B': label = "B"; break; + case 'R': label = "R"; break; + case 'L': label = "L"; break; + case 'A': label = "A"; break; + default: Debug.Assert(false); break; + } + s.AppendLine(" \"" + e.Item1.ToString() + "\" -- " + label + " --> " + " \"" + e.Item3.ToString() + "\";"); + } + s.AppendLine("}"); + s.AppendLine("Initial state: " + initialState); + s.Append("Final states: "); + bool first = true; + foreach (int finalState in finalStates) + { + s.Append((first ? "" : ", ") + finalState); + first = false; + } + s.AppendLine(); + return s.ToString(); + } + } +} -- cgit v1.2.3