| processMainFunction() |   | 4% | | 8% | 6 | 7 | 46 | 51 | 0 | 1 |
| print(PrintWriter, boolean) | | 76% | | 69% | 3 | 9 | 7 | 28 | 0 | 1 |
| setAssumption(SharedVariableIF, ExpressionIF) | | 38% | | 50% | 4 | 5 | 3 | 8 | 0 | 1 |
| locationsWithLabel(String) | | 0% | | 0% | 2 | 2 | 4 | 4 | 1 | 1 |
| newVariable(ScopeIF, TypeIF, String) | | 43% | | 33% | 4 | 6 | 4 | 7 | 0 | 1 |
| setArrayDimensions(VariableIF, ExpressionIF[]) | | 40% | | 50% | 2 | 3 | 2 | 7 | 0 | 1 |
| setCorrespondingVariable(SharedVariableIF, SharedVariableIF) | | 39% | | 50% | 3 | 4 | 3 | 8 | 0 | 1 |
| Model(int, String, int, ModelFactoryIF) | | 74% | | 62% | 3 | 5 | 3 | 19 | 0 | 1 |
| setTargetLocation(StatementIF, LocationIF) | | 49% | | 50% | 1 | 2 | 1 | 6 | 0 | 1 |
| newSharedVariable(TypeIF, String) | | 0% | | n/a | 1 | 1 | 4 | 4 | 1 | 1 |
| addToLocation(LocationIF, CollectiveAssertionIF, ExpressionIF) | | 60% | | 75% | 1 | 3 | 1 | 7 | 0 | 1 |
| newReceiveStatement(ReceiveLocationIF, LHSExpressionIF, ExpressionIF, ExpressionIF, LHSExpressionIF) | | 71% | | 62% | 3 | 5 | 2 | 12 | 0 | 1 |
| setMainFunction(ProcessIF, FunctionIF) | | 50% | | 50% | 1 | 2 | 1 | 5 | 0 | 1 |
| variableDeclaration(VariableIF) | | 68% | | 50% | 1 | 2 | 1 | 5 | 0 | 1 |
| complete() | | 89% | | 88% | 1 | 5 | 1 | 11 | 0 | 1 |
| setLabel(LocationIF, String) | | 67% | | 50% | 1 | 2 | 1 | 5 | 0 | 1 |
| hashCode() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| setCorrespondingLocation(LocationIF, LocationIF) | | 0% | | n/a | 1 | 1 | 2 | 2 | 1 | 1 |
| equals(Object) | | 87% | | 50% | 3 | 4 | 1 | 4 | 0 | 1 |
| argcInput() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| argLengthsInput() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| argsInput() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| argvGlobal() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| isComplete() | | 0% | | n/a | 1 | 1 | 1 | 1 | 1 | 1 |
| newCollectiveAssertion(Sourceable, ProcessIF[], String, boolean, boolean) | | 100% | | 100% | 0 | 3 | 0 | 9 | 0 | 1 |
| newInvocationStatement(InvocationLocationIF, LHSExpressionIF, FunctionIF, List) | | 100% | | 75% | 1 | 3 | 0 | 7 | 0 | 1 |
| newSystemFunction(String, ProcessIF, String, TypeIF, int) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| newFalseBranchStatement(BranchLocationIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| newLoopFalseBranchStatement(LoopLocationIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| newLoopTrueBranchStatement(LoopLocationIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| newTrueBranchStatement(BranchLocationIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| newAllocateStatement(AllocateLocationIF, LHSExpressionIF, TypeIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newFormalVariable(FunctionIF, TypeIF, String, int) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newSendStatement(SendLocationIF, LHSExpressionIF, ExpressionIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newAssertionStatement(AssertionLocationIF, ExpressionIF, String) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newAssignmentStatement(AssignmentLocationIF, LHSExpressionIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newForLoopLocation(LocalScopeIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 5 | 0 | 1 |
| newFunction(ProcessIF, String, TypeIF, int) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newInputVariable(TypeIF, String) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newOutputVariable(TypeIF, String) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newProcessVariable(ProcessIF, TypeIF, String) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newAssertionStatement(AssertionLocationIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newAssumeStatement(AssumeLocationIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newChoiceStatement(ChoiceLocationIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newReturnStatement(ReturnLocationIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newBranchLocation(LocalScopeIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newLoopLocation(LocalScopeIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newAllocateLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newAnySourceReceiveLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newAssertionLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newAssignmentLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newAssumeLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newChoiceLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newInvocationLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newLocalVariable(LocalScope, TypeIF, String) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newReturnLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newSendLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newStandardReceiveLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newTerminalLocation(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| setGuard(SystemFunctionIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| setExitLocation(BranchLocationIF, LocationIF) | | 100% | | n/a | 0 | 1 | 0 | 4 | 0 | 1 |
| newReceiveStatement(ReceiveLocationIF, LHSExpressionIF, ExpressionIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| setStartLocation(FunctionIF, LocationIF) | | 100% | | n/a | 0 | 1 | 0 | 3 | 0 | 1 |
| newLocalScope(LocalScopeIF) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| print(PrintWriter) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| process(int) | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| setInitializationExpression(VariableIF, ExpressionIF) | | 100% | | n/a | 0 | 1 | 0 | 2 | 0 | 1 |
| mainOutput() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| id() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| modelFactory() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| name() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| numProcs() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| toString() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| collectiveAssertions() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |
| scope() | | 100% | | n/a | 0 | 1 | 0 | 1 | 0 | 1 |