public class RulesTransformation extends DepthFirstAdapter
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
COMPUTATION_DISABLED |
static java.lang.String |
COMPUTATION_EXECUTED |
static java.lang.String |
COMPUTATION_NOT_EXECUTED |
static java.lang.String |
RULE_COUNTER_EXAMPLE_VARIABLE_SUFFIX |
static java.lang.String |
RULE_COUNTEREXAMPLE_OUTPUT_PARAMETER_NAME |
static java.lang.String |
RULE_DISABLED |
static java.lang.String |
RULE_FAIL |
static java.lang.String |
RULE_NOT_CHECKED |
static java.lang.String |
RULE_RESULT_OUTPUT_PARAMETER_NAME |
static java.lang.String |
RULE_SUCCESS |
Constructor and Description |
---|
RulesTransformation(Start start,
BParser bParser,
RulesMachineChecker rulesMachineChecker,
java.util.Map<java.lang.String,AbstractOperation> allOperations) |
caseAAbstractConstantsContextClause, caseAAbstractConstantsMachineClause, caseAAbstractMachineParseUnit, caseAAddExpression, caseAAnticipatedEventstatus, caseAAnySubstitution, caseAArityExpression, caseAAssertionsMachineClause, caseAAssertionSubstitution, caseAAssignSubstitution, caseAAxiomsContextClause, caseABecomesElementOfSubstitution, caseABecomesSuchSubstitution, caseABinExpression, caseABlockSubstitution, caseABooleanFalseExpression, caseABooleanTrueExpression, caseABoolSetExpression, caseABtreeExpression, caseACardExpression, caseACartesianProductExpression, caseACaseOrSubstitution, caseACaseSubstitution, caseAChoiceOrSubstitution, caseAChoiceSubstitution, caseAClosureExpression, caseACompositionExpression, caseAComprehensionSetExpression, caseAConcatExpression, caseAConcreteVariablesMachineClause, caseAConjunctPredicate, caseAConstantsContextClause, caseAConstantsMachineClause, caseAConstExpression, caseAConstraintsMachineClause, caseAConstructorFreetypeConstructor, caseAConvergentEventstatus, caseAConversionDefinition, caseAConvertBoolExpression, caseACoupleExpression, caseADefArgpattern, caseADeferredSetSet, caseADefineSubstitution, caseADefinitionExpression, caseADefinitionFileParseUnit, caseADefinitionPredicate, caseADefinitionsMachineClause, caseADefinitionSubstitution, caseADescriptionExpression, caseADescriptionPredicate, caseADescriptionSet, caseADirectProductExpression, caseADisjunctPredicate, caseADivExpression, caseADomainExpression, caseADomainRestrictionExpression, caseADomainSubtractionExpression, caseAElementFreetypeConstructor, caseAEmptySequenceExpression, caseAEmptySetExpression, caseAEnumeratedSetSet, caseAEqualPredicate, caseAEquivalencePredicate, caseAEvent, caseAEventBComprehensionSetExpression, caseAEventBContextParseUnit, caseAEventBFirstProjectionExpression, caseAEventBFirstProjectionV2Expression, caseAEventBIdentityExpression, caseAEventBModelParseUnit, caseAEventBSecondProjectionExpression, caseAEventBSecondProjectionV2Expression, caseAEventsModelClause, caseAExistsPredicate, caseAExpressionDefinition, caseAExpressionDefinitionDefinition, caseAExpressionParseUnit, caseAExpressionsMachineClause, caseAExtendedExprExpression, caseAExtendedPredPredicate, caseAExtendsContextClause, caseAExtendsMachineClause, caseAFalsityPredicate, caseAFatherExpression, caseAFileDefinitionDefinition, caseAFileExpression, caseAFileMachineReference, caseAFin1SubsetExpression, caseAFinitePredicate, caseAFinSubsetExpression, caseAFirstExpression, caseAFirstProjectionExpression, caseAFlooredDivExpression, caseAForallPredicate, caseAForallSubMessageSubstitution, caseAForLoopSubstitution, caseAFreetype, caseAFreetypesMachineClause, caseAFrontExpression, caseAFuncOpSubstitution, caseAFunctionExpression, caseAFunctionOperation, caseAGeneralConcatExpression, caseAGeneralIntersectionExpression, caseAGeneralProductExpression, caseAGeneralSumExpression, caseAGeneralUnionExpression, caseAGeneratedParseUnit, caseAGreaterEqualPredicate, caseAGreaterPredicate, caseAIdentifierExpression, caseAIdentityExpression, caseAIfElsifSubstitution, caseAIfPredicatePredicate, caseAIfSubstitution, caseAIfThenElseExpression, caseAImageExpression, caseAImplementationMachineParseUnit, caseAImplicationPredicate, caseAImportPackage, caseAImportsMachineClause, caseAIncludesMachineClause, caseAInferredUnitExpression, caseAInfixExpression, caseAInitialisationMachineClause, caseAInsertFrontExpression, caseAInsertTailExpression, caseAIntegerExpression, caseAIntegerSetExpression, caseAIntersectionExpression, caseAIntervalExpression, caseAIntSetExpression, caseAInvalidOperationsClauseMachineClause, caseAInvalidSubstitution, caseAInvariantMachineClause, caseAInvariantModelClause, caseAIseq1Expression, caseAIseqExpression, caseAIterationExpression, caseALabelPredicate, caseALambdaExpression, caseALastExpression, caseALeftExpression, caseALessEqualPredicate, caseALessPredicate, caseALetExpressionExpression, caseALetPredicatePredicate, caseALetSubstitution, caseALocalOperationsMachineClause, caseAMachineClauseParseUnit, caseAMachineHeader, caseAMachineMachineVariant, caseAMachineReference, caseAMaxExpression, caseAMaxIntExpression, caseAMemberPredicate, caseAMinExpression, caseAMinIntExpression, caseAMinusExpression, caseAMinusOrSetSubtractExpression, caseAMirrorExpression, caseAMissingSemicolonOperation, caseAModelMachineVariant, caseAModuloExpression, caseAMultilineStringExpression, caseAMultiplicationExpression, caseAMultOrCartExpression, caseANat1SetExpression, caseANatSetExpression, caseANatural1SetExpression, caseANaturalSetExpression, caseANegationPredicate, caseANewUnitExpression, caseANotEqualPredicate, caseANotMemberPredicate, caseANotSubsetPredicate, caseANotSubsetStrictPredicate, caseAOperation, caseAOperationAttribute, caseAOperationCallExpression, caseAOperationCallSubstitution, caseAOperationsMachineClause, caseAOperatorExpression, caseAOperatorPredicate, caseAOperatorSubstitution, caseAOppatternParseUnit, caseAOpSubstitution, caseAOrdinaryEventstatus, caseAOverwriteExpression, caseAPackageParseUnit, caseAParallelProductExpression, caseAParallelSubstitution, caseAParseUnitDefinitionParseUnit, caseAPartialBijectionExpression, caseAPartialFunctionExpression, caseAPartialInjectionExpression, caseAPartialSurjectionExpression, caseAPartitionPredicate, caseAPermExpression, caseAPostfixExpression, caseAPow1SubsetExpression, caseAPowerOfExpression, caseAPowSubsetExpression, caseAPreconditionSubstitution, caseAPredecessorExpression, caseAPredicateAttributeOperationAttribute, caseAPredicateDefinition, caseAPredicateDefinitionDefinition, caseAPredicateFunctionPredicate, caseAPredicateIdentifierPredicate, caseAPredicateParseUnit, caseAPredicatesMachineClause, caseAPrefixExpression, caseAPrimedIdentifierExpression, caseAPromotesMachineClause, caseAPropertiesMachineClause, caseAProverComprehensionSetExpression, caseAQuantifiedIntersectionExpression, caseAQuantifiedUnionExpression, caseARangeExpression, caseARangeRestrictionExpression, caseARangeSubtractionExpression, caseARankExpression, caseARecEntry, caseARecExpression, caseARecordFieldExpression, caseAReferencesMachineClause, caseARefinementMachineParseUnit, caseARefinesModelClause, caseAReflexiveClosureExpression, caseARelationsExpression, caseARestrictFrontExpression, caseARestrictTailExpression, caseAReverseExpression, caseARevExpression, caseARightExpression, caseARingExpression, caseARuleFailSubSubstitution, caseASecondProjectionExpression, caseASeesMachineClause, caseASeesModelClause, caseASelectSubstitution, caseASelectWhenSubstitution, caseASeq1Expression, caseASeqExpression, caseASequenceExtensionExpression, caseASequenceSubstitution, caseASetExtensionExpression, caseASetsContextClause, caseASetsMachineClause, caseASetSubtractionExpression, caseASizeExpression, caseASizetExpression, caseASkipSubstitution, caseASonExpression, caseASonsExpression, caseAStringExpression, caseAStringSetExpression, caseAStructExpression, caseASubsetPredicate, caseASubsetStrictPredicate, caseASubstitutionDefinitionDefinition, caseASubstitutionParseUnit, caseASubstitutionPredicate, caseASubtreeExpression, caseASuccessorExpression, caseASurjectionRelationExpression, caseASymbolicComprehensionSetExpression, caseASymbolicLambdaExpression, caseASystemMachineVariant, caseATailExpression, caseATheoremsContextClause, caseATheoremsModelClause, caseATopExpression, caseATotalBijectionExpression, caseATotalFunctionExpression, caseATotalInjectionExpression, caseATotalRelationExpression, caseATotalSurjectionExpression, caseATotalSurjectionRelationExpression, caseATransFunctionExpression, caseATransRelationExpression, caseATreeExpression, caseATruthPredicate, caseATypeofExpression, caseAUnaryMinusExpression, caseAUndefArgpattern, caseAUnionExpression, caseAUnitAliasParseUnit, caseAUnitExpression, caseAUsesMachineClause, caseAValuesEntry, caseAValuesMachineClause, caseAVariablesMachineClause, caseAVariablesModelClause, caseAVariantModelClause, caseAVarSubstitution, caseAWhileSubstitution, caseAWitness, caseStart, defaultIn, defaultOut, inAAbstractConstantsContextClause, inAAbstractConstantsMachineClause, inAAbstractMachineParseUnit, inAAddExpression, inAAnticipatedEventstatus, inAAnySubstitution, inAArityExpression, inAAssertionsMachineClause, inAAssertionSubstitution, inAAssignSubstitution, inAAxiomsContextClause, inABecomesElementOfSubstitution, inABecomesSuchSubstitution, inABinExpression, inABlockSubstitution, inABooleanFalseExpression, inABooleanTrueExpression, inABoolSetExpression, inABtreeExpression, inACardExpression, inACartesianProductExpression, inACaseOrSubstitution, inACaseSubstitution, inAChoiceOrSubstitution, inAChoiceSubstitution, inAClosureExpression, inACompositionExpression, inAComprehensionSetExpression, inAComputationOperation, inAConcatExpression, inAConcreteVariablesMachineClause, inAConjunctPredicate, inAConstantsContextClause, inAConstantsMachineClause, inAConstExpression, inAConstraintsMachineClause, inAConstructorFreetypeConstructor, inAConvergentEventstatus, inAConversionDefinition, inAConvertBoolExpression, inACoupleExpression, inADefArgpattern, inADeferredSetSet, inADefineSubstitution, inADefinitionExpression, inADefinitionFileParseUnit, inADefinitionPredicate, inADefinitionsMachineClause, inADefinitionSubstitution, inADescriptionExpression, inADescriptionPredicate, inADescriptionSet, inADirectProductExpression, inADisjunctPredicate, inADivExpression, inADomainExpression, inADomainRestrictionExpression, inADomainSubtractionExpression, inAElementFreetypeConstructor, inAEmptySequenceExpression, inAEmptySetExpression, inAEnumeratedSetSet, inAEqualPredicate, inAEquivalencePredicate, inAEvent, inAEventBComprehensionSetExpression, inAEventBContextParseUnit, inAEventBFirstProjectionExpression, inAEventBFirstProjectionV2Expression, inAEventBIdentityExpression, inAEventBModelParseUnit, inAEventBSecondProjectionExpression, inAEventBSecondProjectionV2Expression, inAEventsModelClause, inAExistsPredicate, inAExpressionDefinition, inAExpressionDefinitionDefinition, inAExpressionParseUnit, inAExpressionsMachineClause, inAExtendedExprExpression, inAExtendedPredPredicate, inAExtendsContextClause, inAExtendsMachineClause, inAFalsityPredicate, inAFatherExpression, inAFileDefinitionDefinition, inAFileExpression, inAFileMachineReference, inAFin1SubsetExpression, inAFinitePredicate, inAFinSubsetExpression, inAFirstExpression, inAFirstProjectionExpression, inAFlooredDivExpression, inAForallPredicate, inAForallSubMessageSubstitution, inAFreetype, inAFreetypesMachineClause, inAFrontExpression, inAFuncOpSubstitution, inAFunctionExpression, inAFunctionOperation, inAGeneralConcatExpression, inAGeneralIntersectionExpression, inAGeneralProductExpression, inAGeneralSumExpression, inAGeneralUnionExpression, inAGeneratedParseUnit, inAGreaterEqualPredicate, inAGreaterPredicate, inAIdentifierExpression, inAIdentityExpression, inAIfElsifSubstitution, inAIfPredicatePredicate, inAIfSubstitution, inAIfThenElseExpression, inAImageExpression, inAImplementationMachineParseUnit, inAImplicationPredicate, inAImportPackage, inAImportsMachineClause, inAIncludesMachineClause, inAInferredUnitExpression, inAInfixExpression, inAInitialisationMachineClause, inAInsertFrontExpression, inAInsertTailExpression, inAIntegerExpression, inAIntegerSetExpression, inAIntersectionExpression, inAIntervalExpression, inAIntSetExpression, inAInvalidOperationsClauseMachineClause, inAInvalidSubstitution, inAInvariantMachineClause, inAInvariantModelClause, inAIseq1Expression, inAIseqExpression, inAIterationExpression, inALabelPredicate, inALambdaExpression, inALastExpression, inALeftExpression, inALessEqualPredicate, inALessPredicate, inALetExpressionExpression, inALetPredicatePredicate, inALetSubstitution, inALocalOperationsMachineClause, inAMachineClauseParseUnit, inAMachineHeader, inAMachineMachineVariant, inAMachineReference, inAMaxExpression, inAMaxIntExpression, inAMemberPredicate, inAMinExpression, inAMinIntExpression, inAMinusExpression, inAMinusOrSetSubtractExpression, inAMirrorExpression, inAMissingSemicolonOperation, inAModelMachineVariant, inAModuloExpression, inAMultilineStringExpression, inAMultiplicationExpression, inAMultOrCartExpression, inANat1SetExpression, inANatSetExpression, inANatural1SetExpression, inANaturalSetExpression, inANegationPredicate, inANewUnitExpression, inANotEqualPredicate, inANotMemberPredicate, inANotSubsetPredicate, inANotSubsetStrictPredicate, inAOperation, inAOperationAttribute, inAOperationCallExpression, inAOperationCallSubstitution, inAOperationsMachineClause, inAOperatorExpression, inAOperatorPredicate, inAOperatorSubstitution, inAOppatternParseUnit, inAOpSubstitution, inAOrdinaryEventstatus, inAOverwriteExpression, inAPackageParseUnit, inAParallelProductExpression, inAParallelSubstitution, inAParseUnitDefinitionParseUnit, inAPartialBijectionExpression, inAPartialFunctionExpression, inAPartialInjectionExpression, inAPartialSurjectionExpression, inAPartitionPredicate, inAPermExpression, inAPostfixExpression, inAPow1SubsetExpression, inAPowerOfExpression, inAPowSubsetExpression, inAPreconditionSubstitution, inAPredecessorExpression, inAPredicateAttributeOperationAttribute, inAPredicateDefinition, inAPredicateDefinitionDefinition, inAPredicateFunctionPredicate, inAPredicateIdentifierPredicate, inAPredicateParseUnit, inAPredicatesMachineClause, inAPrefixExpression, inAPrimedIdentifierExpression, inAPromotesMachineClause, inAPropertiesMachineClause, inAProverComprehensionSetExpression, inAQuantifiedIntersectionExpression, inAQuantifiedUnionExpression, inARangeExpression, inARangeRestrictionExpression, inARangeSubtractionExpression, inARankExpression, inARecEntry, inARecExpression, inARecordFieldExpression, inAReferencesMachineClause, inARefinementMachineParseUnit, inARefinesModelClause, inAReflexiveClosureExpression, inARelationsExpression, inARestrictFrontExpression, inARestrictTailExpression, inAReverseExpression, inARevExpression, inARightExpression, inARingExpression, inARuleFailSubSubstitution, inASecondProjectionExpression, inASeesMachineClause, inASeesModelClause, inASelectSubstitution, inASelectWhenSubstitution, inASeq1Expression, inASeqExpression, inASequenceExtensionExpression, inASequenceSubstitution, inASetExtensionExpression, inASetsContextClause, inASetsMachineClause, inASetSubtractionExpression, inASizeExpression, inASizetExpression, inASkipSubstitution, inASonExpression, inASonsExpression, inAStringExpression, inAStringSetExpression, inAStructExpression, inASubsetPredicate, inASubsetStrictPredicate, inASubstitutionDefinitionDefinition, inASubstitutionParseUnit, inASubstitutionPredicate, inASubtreeExpression, inASuccessorExpression, inASurjectionRelationExpression, inASymbolicComprehensionSetExpression, inASymbolicLambdaExpression, inASystemMachineVariant, inATailExpression, inATheoremsContextClause, inATheoremsModelClause, inATopExpression, inATotalBijectionExpression, inATotalFunctionExpression, inATotalInjectionExpression, inATotalRelationExpression, inATotalSurjectionExpression, inATotalSurjectionRelationExpression, inATransFunctionExpression, inATransRelationExpression, inATreeExpression, inATruthPredicate, inATypeofExpression, inAUnaryMinusExpression, inAUndefArgpattern, inAUnionExpression, inAUnitAliasParseUnit, inAUnitExpression, inAUsesMachineClause, inAValuesEntry, inAValuesMachineClause, inAVariablesMachineClause, inAVariablesModelClause, inAVariantModelClause, inAVarSubstitution, inAWhileSubstitution, inAWitness, inStart, outAAbstractConstantsContextClause, outAAbstractConstantsMachineClause, outAAbstractMachineParseUnit, outAAddExpression, outAAnticipatedEventstatus, outAAnySubstitution, outAArityExpression, outAAssertionsMachineClause, outAAssertionSubstitution, outAAssignSubstitution, outAAxiomsContextClause, outABecomesElementOfSubstitution, outABecomesSuchSubstitution, outABinExpression, outABlockSubstitution, outABooleanFalseExpression, outABooleanTrueExpression, outABoolSetExpression, outABtreeExpression, outACardExpression, outACartesianProductExpression, outACaseOrSubstitution, outACaseSubstitution, outAChoiceOrSubstitution, outAChoiceSubstitution, outAClosureExpression, outACompositionExpression, outAComprehensionSetExpression, outAConcatExpression, outAConcreteVariablesMachineClause, outAConjunctPredicate, outAConstantsContextClause, outAConstantsMachineClause, outAConstExpression, outAConstraintsMachineClause, outAConstructorFreetypeConstructor, outAConvergentEventstatus, outAConversionDefinition, outAConvertBoolExpression, outACoupleExpression, outADefArgpattern, outADeferredSetSet, outADefinitionExpression, outADefinitionFileParseUnit, outADefinitionPredicate, outADefinitionsMachineClause, outADefinitionSubstitution, outADescriptionExpression, outADescriptionPredicate, outADescriptionSet, outADirectProductExpression, outADisjunctPredicate, outADivExpression, outADomainExpression, outADomainRestrictionExpression, outADomainSubtractionExpression, outAElementFreetypeConstructor, outAEmptySequenceExpression, outAEmptySetExpression, outAEnumeratedSetSet, outAEqualPredicate, outAEquivalencePredicate, outAEvent, outAEventBComprehensionSetExpression, outAEventBContextParseUnit, outAEventBFirstProjectionExpression, outAEventBFirstProjectionV2Expression, outAEventBIdentityExpression, outAEventBModelParseUnit, outAEventBSecondProjectionExpression, outAEventBSecondProjectionV2Expression, outAEventsModelClause, outAExistsPredicate, outAExpressionDefinition, outAExpressionDefinitionDefinition, outAExpressionParseUnit, outAExpressionsMachineClause, outAExtendedExprExpression, outAExtendedPredPredicate, outAExtendsContextClause, outAExtendsMachineClause, outAFalsityPredicate, outAFatherExpression, outAFileDefinitionDefinition, outAFileExpression, outAFileMachineReference, outAFin1SubsetExpression, outAFinitePredicate, outAFinSubsetExpression, outAFirstExpression, outAFirstProjectionExpression, outAFlooredDivExpression, outAForallPredicate, outAFreetype, outAFreetypesMachineClause, outAFrontExpression, outAFuncOpSubstitution, outAFunctionExpression, outAGeneralConcatExpression, outAGeneralIntersectionExpression, outAGeneralProductExpression, outAGeneralSumExpression, outAGeneralUnionExpression, outAGeneratedParseUnit, outAGreaterEqualPredicate, outAGreaterPredicate, outAIdentifierExpression, outAIdentityExpression, outAIfElsifSubstitution, outAIfPredicatePredicate, outAIfSubstitution, outAIfThenElseExpression, outAImageExpression, outAImplementationMachineParseUnit, outAImplicationPredicate, outAImportPackage, outAImportsMachineClause, outAIncludesMachineClause, outAInferredUnitExpression, outAInfixExpression, outAInitialisationMachineClause, outAInsertFrontExpression, outAInsertTailExpression, outAIntegerExpression, outAIntegerSetExpression, outAIntersectionExpression, outAIntervalExpression, outAIntSetExpression, outAInvalidOperationsClauseMachineClause, outAInvalidSubstitution, outAInvariantMachineClause, outAInvariantModelClause, outAIseq1Expression, outAIseqExpression, outAIterationExpression, outALabelPredicate, outALambdaExpression, outALastExpression, outALeftExpression, outALessEqualPredicate, outALessPredicate, outALetExpressionExpression, outALetPredicatePredicate, outALetSubstitution, outALocalOperationsMachineClause, outAMachineClauseParseUnit, outAMachineHeader, outAMachineMachineVariant, outAMachineReference, outAMaxExpression, outAMaxIntExpression, outAMemberPredicate, outAMinExpression, outAMinIntExpression, outAMinusExpression, outAMinusOrSetSubtractExpression, outAMirrorExpression, outAMissingSemicolonOperation, outAModelMachineVariant, outAModuloExpression, outAMultilineStringExpression, outAMultiplicationExpression, outAMultOrCartExpression, outANat1SetExpression, outANatSetExpression, outANatural1SetExpression, outANaturalSetExpression, outANegationPredicate, outANewUnitExpression, outANotEqualPredicate, outANotMemberPredicate, outANotSubsetPredicate, outANotSubsetStrictPredicate, outAOperation, outAOperationAttribute, outAOperationCallExpression, outAOperationCallSubstitution, outAOperationsMachineClause, outAOperatorSubstitution, outAOppatternParseUnit, outAOpSubstitution, outAOrdinaryEventstatus, outAOverwriteExpression, outAPackageParseUnit, outAParallelProductExpression, outAParallelSubstitution, outAParseUnitDefinitionParseUnit, outAPartialBijectionExpression, outAPartialFunctionExpression, outAPartialInjectionExpression, outAPartialSurjectionExpression, outAPartitionPredicate, outAPermExpression, outAPostfixExpression, outAPow1SubsetExpression, outAPowerOfExpression, outAPowSubsetExpression, outAPreconditionSubstitution, outAPredecessorExpression, outAPredicateAttributeOperationAttribute, outAPredicateDefinition, outAPredicateDefinitionDefinition, outAPredicateFunctionPredicate, outAPredicateIdentifierPredicate, outAPredicateParseUnit, outAPredicatesMachineClause, outAPrefixExpression, outAPrimedIdentifierExpression, outAPromotesMachineClause, outAPropertiesMachineClause, outAProverComprehensionSetExpression, outAQuantifiedIntersectionExpression, outAQuantifiedUnionExpression, outARangeExpression, outARangeRestrictionExpression, outARangeSubtractionExpression, outARankExpression, outARecEntry, outARecExpression, outARecordFieldExpression, outAReferencesMachineClause, outARefinementMachineParseUnit, outARefinesModelClause, outAReflexiveClosureExpression, outARelationsExpression, outARestrictFrontExpression, outARestrictTailExpression, outAReverseExpression, outARevExpression, outARightExpression, outARingExpression, outASecondProjectionExpression, outASeesMachineClause, outASeesModelClause, outASelectSubstitution, outASelectWhenSubstitution, outASeq1Expression, outASeqExpression, outASequenceExtensionExpression, outASequenceSubstitution, outASetExtensionExpression, outASetsContextClause, outASetsMachineClause, outASetSubtractionExpression, outASizeExpression, outASizetExpression, outASkipSubstitution, outASonExpression, outASonsExpression, outAStringExpression, outAStringSetExpression, outAStructExpression, outASubsetPredicate, outASubsetStrictPredicate, outASubstitutionDefinitionDefinition, outASubstitutionParseUnit, outASubstitutionPredicate, outASubtreeExpression, outASuccessorExpression, outASurjectionRelationExpression, outASymbolicComprehensionSetExpression, outASymbolicLambdaExpression, outASystemMachineVariant, outATailExpression, outATheoremsContextClause, outATheoremsModelClause, outATopExpression, outATotalBijectionExpression, outATotalFunctionExpression, outATotalInjectionExpression, outATotalRelationExpression, outATotalSurjectionExpression, outATotalSurjectionRelationExpression, outATransFunctionExpression, outATransRelationExpression, outATreeExpression, outATruthPredicate, outATypeofExpression, outAUnaryMinusExpression, outAUndefArgpattern, outAUnionExpression, outAUnitAliasParseUnit, outAUnitExpression, outAUsesMachineClause, outAValuesEntry, outAValuesMachineClause, outAVariablesMachineClause, outAVariablesModelClause, outAVariantModelClause, outAVarSubstitution, outAWhileSubstitution, outAWitness
caseEOF, caseTAbstractConstants, caseTAbstractVariables, caseTAny, caseTArity, caseTAssert, caseTAssertions, caseTAssign, caseTBe, caseTBegin, caseTBfalse, caseTBin, caseTBool, caseTBoolCast, caseTBtree, caseTCard, caseTCase, caseTChoice, caseTClosure, caseTClosure1, caseTComma, caseTComment, caseTCommentBody, caseTCommentEnd, caseTConc, caseTConcatSequence, caseTConcreteConstants, caseTConcreteVariables, caseTConjunction, caseTConst, caseTConstants, caseTConstraints, caseTDefinitions, caseTDefLiteralPredicate, caseTDefLiteralSubstitution, caseTDirectProduct, caseTDivision, caseTDo, caseTDollar, caseTDom, caseTDomainRestriction, caseTDomainSubtraction, caseTDot, caseTDoubleColon, caseTDoubleEqual, caseTDoubleVerticalBar, caseTEither, caseTElementOf, caseTElse, caseTElsif, caseTEmptySet, caseTEnd, caseTEqual, caseTEquivalence, caseTExists, caseTExpressions, caseTExtends, caseTFalse, caseTFather, caseTFin, caseTFin1, caseTFirst, caseTFnc, caseTForAny, caseTFront, caseTGeneralizedInter, caseTGeneralizedUnion, caseTGreater, caseTGreaterEqual, caseTHexLiteral, caseTId, caseTIdentifierLiteral, caseTIf, caseTImplementation, caseTImplies, caseTImports, caseTIn, caseTIncludes, caseTInclusion, caseTInfix, caseTInitialisation, caseTInsertEndSequence, caseTInsertStartSequence, caseTInt, caseTInteger, caseTIntegerLiteral, caseTIntersection, caseTInterval, caseTInvariant, caseTIpragmaUnit, caseTIseq, caseTIseq1, caseTIterate, caseTKwAbstractConstants, caseTKwAbstractVariables, caseTKwAssertions, caseTKwAttributeIdentifier, caseTKwBody, caseTKwComputation, caseTKwConcreteConstants, caseTKwConcreteVariables, caseTKwConstants, caseTKwConstraints, caseTKwCounterexample, caseTKwDefine, caseTKwDefinition, caseTKwDefinitions, caseTKwDummyValue, caseTKwExpect, caseTKwExpression, caseTKwExpressionOperator, caseTKwExtends, caseTKwFor, caseTKwFormula, caseTKwFreetypes, caseTKwFunction, caseTKwImports, caseTKwIncludes, caseTKwInitialisation, caseTKwInvariant, caseTKwLocalOperations, caseTKwMachineClause, caseTKwOperations, caseTKwOppattern, caseTKwPredicate, caseTKwPredicateAttribute, caseTKwPredicateOperator, caseTKwPromotes, caseTKwProperties, caseTKwReferences, caseTKwRule, caseTKwRuleErrorType, caseTKwRuleFail, caseTKwRuleForAll, caseTKwRulesMachine, caseTKwSees, caseTKwSets, caseTKwSubstitution, caseTKwSubstitutionOperator, caseTKwType, caseTKwUses, caseTKwValue, caseTKwValues, caseTKwVariables, caseTLambda, caseTLast, caseTLeft, caseTLeftBrace, caseTLeftBracket, caseTLeftPar, caseTLess, caseTLessEqual, caseTLet, caseTLineComment, caseTLocalOperations, caseTLogicalOr, caseTMachine, caseTMaplet, caseTMax, caseTMaxInt, caseTMin, caseTMinInt, caseTMinus, caseTMirror, caseTMod, caseTModel, caseTMultilineStringContent, caseTMultilineStringEnd, caseTMultilineStringStart, caseTNat, caseTNat1, caseTNatural, caseTNatural1, caseTNewPragmaUnit, caseTNonInclusion, caseTNot, caseTNotBelonging, caseTNotEqual, caseTOf, caseTOperations, caseTOr, caseTOutputParameters, caseTOverwriteRelation, caseTPartialBijection, caseTPartialFunction, caseTPartialInjection, caseTPartialSurjection, caseTPerm, caseTPi, caseTPlus, caseTPostfix, caseTPow, caseTPow1, caseTPowerOf, caseTPragmaConversion, caseTPragmaDescription, caseTPragmaEnd, caseTPragmaFile, caseTPragmaFreeText, caseTPragmaGenerated, caseTPragmaIdOrString, caseTPragmaImportPackage, caseTPragmaLabel, caseTPragmaPackage, caseTPragmaStart, caseTPragmaSymbolic, caseTPragmaUnit, caseTPragmaUnitAlias, caseTPre, caseTPred, caseTPredicateIdentifier, caseTPredicates, caseTPrefix, caseTPrj1, caseTPrj2, caseTProduct, caseTPromotes, caseTProperties, caseTQuantifiedInter, caseTQuantifiedSet, caseTQuantifiedUnion, caseTRan, caseTRangeRestriction, caseTRangeSubtraction, caseTRank, caseTRec, caseTRefinement, caseTRefines, caseTRel, caseTRestrictHeadSequence, caseTRestrictTailSequence, caseTRev, caseTRight, caseTRightBrace, caseTRightBracket, caseTRightPar, caseTSees, caseTSelect, caseTSemicolon, caseTSeq, caseTSeq1, caseTSetRelation, caseTSets, caseTSetSubtraction, caseTShebang, caseTShebangChar, caseTShebangEnd, caseTSigma, caseTSingleQuotation, caseTSize, caseTSizet, caseTSkip, caseTSlash, caseTSon, caseTSons, caseTStar, caseTStrictInclusion, caseTStrictNonInclusion, caseTString, caseTStringLiteral, caseTStruct, caseTSubtree, caseTSucc, caseTSurjectionRelation, caseTSystem, caseTTail, caseTThen, caseTTilde, caseTTop, caseTTotalBijection, caseTTotalFunction, caseTTotalInjection, caseTTotalRelation, caseTTotalSurjection, caseTTotalSurjectionRelation, caseTTree, caseTTrue, caseTTruthPredicate, caseTUnderscore, caseTUnion, caseTUnitContent, caseTUnitId, caseTUses, caseTValue, caseTVar, caseTVariables, caseTVariant, caseTVerticalBar, caseTWhen, caseTWhere, caseTWhile, caseTWhiteSpace, defaultCase, getIn, getOut, setIn, setOut
public static final java.lang.String RULE_FAIL
public static final java.lang.String RULE_SUCCESS
public static final java.lang.String RULE_NOT_CHECKED
public static final java.lang.String RULE_DISABLED
public static final java.lang.String COMPUTATION_EXECUTED
public static final java.lang.String COMPUTATION_NOT_EXECUTED
public static final java.lang.String COMPUTATION_DISABLED
public static final java.lang.String RULE_RESULT_OUTPUT_PARAMETER_NAME
public static final java.lang.String RULE_COUNTEREXAMPLE_OUTPUT_PARAMETER_NAME
public static final java.lang.String RULE_COUNTER_EXAMPLE_VARIABLE_SUFFIX
public RulesTransformation(Start start, BParser bParser, RulesMachineChecker rulesMachineChecker, java.util.Map<java.lang.String,AbstractOperation> allOperations)
start
- The root node of the abstract syntax tree.bParser
- The parser of the rules machine.rulesMachineChecker
- the rules machine checker which has already analyzed the rules
machineallOperations
- The list of all operation in the project. This parameter is
needed in order to detect invalid reference to operations
which does not exist. Note, that such checks can not be done
by the RulesMachineChecker
because they need more than
the machine scope. For example, it is checked that the first
argument of the GET_RULE_COUNTEREXAMPLES operator is an
existing rule operation which may be located in another rules
machine.public void runTransformation() throws BCompoundException
BCompoundException
public java.util.List<AbstractOperation> getOperations()
public java.util.List<java.lang.String> getComputations()
public void outStart(Start node)
outStart
in class DepthFirstAdapter
public void caseAComputationOperation(AComputationOperation node)
caseAComputationOperation
in interface Analysis
caseAComputationOperation
in class DepthFirstAdapter
public java.util.List<PPredicate> getOperationDependenciesAsPredicateList(AbstractOperation operation)
public void outAComputationOperation(AComputationOperation node)
outAComputationOperation
in class DepthFirstAdapter
public void caseARuleOperation(ARuleOperation node)
caseARuleOperation
in interface Analysis
caseARuleOperation
in class DepthFirstAdapter
public void inARuleOperation(ARuleOperation node)
inARuleOperation
in class DepthFirstAdapter
public void outARuleOperation(ARuleOperation node)
outARuleOperation
in class DepthFirstAdapter
public void outAOperatorExpression(AOperatorExpression node)
outAOperatorExpression
in class DepthFirstAdapter
public void outADefineSubstitution(ADefineSubstitution node)
outADefineSubstitution
in class DepthFirstAdapter
public void outAFunctionOperation(AFunctionOperation node)
outAFunctionOperation
in class DepthFirstAdapter
public void outAOperatorPredicate(AOperatorPredicate node)
outAOperatorPredicate
in class DepthFirstAdapter
public void inAForLoopSubstitution(AForLoopSubstitution node)
inAForLoopSubstitution
in class DepthFirstAdapter
public void outAForLoopSubstitution(AForLoopSubstitution node)
outAForLoopSubstitution
in class DepthFirstAdapter
public void outARuleFailSubSubstitution(ARuleFailSubSubstitution node)
outARuleFailSubSubstitution
in class DepthFirstAdapter
public PSubstitution createCounterExampleSubstitutions(java.util.List<PExpression> identifiers, PPredicate wherePredicate, PPredicate expectPredicate, PExpression message, TIntegerLiteral errorTypeNode)
public void outAForallSubMessageSubstitution(AForallSubMessageSubstitution node)
outAForallSubMessageSubstitution
in class DepthFirstAdapter