diff options
Diffstat (limited to 'rba.tool.editor/src/rba/tool/editor/generator')
16 files changed, 4051 insertions, 0 deletions
diff --git a/rba.tool.editor/src/rba/tool/editor/generator/RBAModelGeneratorDelegate.xtend b/rba.tool.editor/src/rba/tool/editor/generator/RBAModelGeneratorDelegate.xtend new file mode 100644 index 0000000..5d0b582 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/RBAModelGeneratorDelegate.xtend @@ -0,0 +1,184 @@ +package rba.tool.editor.generator + +import com.google.inject.Inject +import java.util.Set +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.emf.ecore.resource.ResourceSet +import org.eclipse.xtext.generator.GeneratorContext +import org.eclipse.xtext.generator.IFileSystemAccess +import org.eclipse.xtext.generator.IFileSystemAccess2 +import org.eclipse.xtext.generator.IGenerator +import org.eclipse.xtext.generator.IGenerator2 +import org.eclipse.xtext.generator.IGeneratorContext +import org.eclipse.xtext.generator.OutputConfiguration +import org.eclipse.xtext.util.CancelIndicator +import rba.tool.editor.generator.json.IJSONGenerator +import rba.tool.editor.generator.rtmodel.IRTModelUpdater +import rba.tool.editor.generator.z3.IConstraintGenerator +import rba.tool.editor.generator.z3.ISortValueGenerator + +class RBAModelGeneratorDelegate implements IGenerator, IGenerator2 { + + @Inject(optional=true) + private ISortValueGenerator sortValueGenerator; + + private ThreadLocal<Boolean> sortValueGeneratorInBuilding = new ThreadLocal<Boolean>() { + override protected initialValue() { + return false; + } + }; + + @Inject(optional=true) + private IRTModelUpdater rtModelUpdater; + + private ThreadLocal<Boolean> rtModelUpdaterInBuilding = new ThreadLocal<Boolean>() { + override protected initialValue() { + return false; + } + }; + + @Inject(optional=true) + private IConstraintGenerator constraintGenerator; + + private ThreadLocal<Boolean> constraintGeneratorInBuilding = new ThreadLocal<Boolean>() { + override protected initialValue() { + return false; + } + }; + + @Inject(optional=true) + private IJSONGenerator jsonGenerator; + + private ThreadLocal<Boolean> jsonGeneratorInBuilding = new ThreadLocal<Boolean>() { + override protected initialValue() { + return false; + } + }; + + def public void generate(Resource input, IFileSystemAccess2 fsa, IGeneratorContext context) { + generate(input.resourceSet, fsa, context); + } + + def public void generate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + if (sortValueGenerator !== null && !sortValueGeneratorInBuilding.get.booleanValue) { + sortValueGeneratorInBuilding.set(true); + } + if (rtModelUpdater !== null && !rtModelUpdaterInBuilding.get.booleanValue) { + rtModelUpdaterInBuilding.set(true); + } + if (constraintGenerator !== null && !constraintGeneratorInBuilding.get.booleanValue) { + constraintGeneratorInBuilding.set(true); + } + if (jsonGenerator !== null && !jsonGeneratorInBuilding.get.booleanValue) { + jsonGeneratorInBuilding.set(true); + } + + try { + beforeGenerate(input, fsa, context); + doGenerate(input, fsa, context); + } finally { + afterGenerate(input, fsa, context); + } + } + + override doGenerate(Resource input, IFileSystemAccess2 fsa, IGeneratorContext context) { + doGenerate(input.resourceSet, fsa, context); + } + + def void doGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + if (sortValueGenerator !== null && sortValueGeneratorInBuilding.get.booleanValue) { + sortValueGenerator.doGenerate(input, fsa, context); + } + if (rtModelUpdater !== null && rtModelUpdaterInBuilding.get.booleanValue) { + rtModelUpdater.doGenerate(input, fsa, context); + } + if (constraintGenerator !== null && constraintGeneratorInBuilding.get.booleanValue) { + constraintGenerator.doGenerate(input, fsa, context); + } + if (jsonGenerator !== null && jsonGeneratorInBuilding.get.booleanValue) { + jsonGenerator.doGenerate(input, fsa, context); + } + } + + override beforeGenerate(Resource input, IFileSystemAccess2 fsa, IGeneratorContext context) { + beforeGenerate(input.resourceSet, fsa, context); + } + + def void beforeGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + if (sortValueGenerator !== null && sortValueGeneratorInBuilding.get.booleanValue) { + sortValueGenerator.beforeGenerate(input, fsa, context); + } + if (rtModelUpdater !== null && rtModelUpdaterInBuilding.get.booleanValue) { + rtModelUpdater.beforeGenerate(input, fsa, context); + } + if (constraintGenerator !== null && constraintGeneratorInBuilding.get.booleanValue) { + constraintGenerator.beforeGenerate(input, fsa, context); + } + if (jsonGenerator !== null && jsonGeneratorInBuilding.get.booleanValue) { + jsonGenerator.beforeGenerate(input, fsa, context); + } + } + + override afterGenerate(Resource input, IFileSystemAccess2 fsa, IGeneratorContext context) { + afterGenerate(input.resourceSet, fsa, context); + } + + def void afterGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + if (sortValueGenerator !== null && sortValueGeneratorInBuilding.get.booleanValue) { + sortValueGenerator.afterGenerate(input, fsa, context); + } + if (rtModelUpdater !== null && rtModelUpdaterInBuilding.get.booleanValue) { + rtModelUpdater.afterGenerate(input, fsa, context); + } + if (constraintGenerator !== null && constraintGeneratorInBuilding.get.booleanValue) { + constraintGenerator.afterGenerate(input, fsa, context); + } + if (jsonGenerator !== null && jsonGeneratorInBuilding.get.booleanValue) { + jsonGenerator.afterGenerate(input, fsa, context); + } + } + + override doGenerate(Resource input, IFileSystemAccess fsa) { + doGenerate(input.resourceSet, fsa); + } + + def void doGenerate(ResourceSet input, IFileSystemAccess fsa) { + val casted = fsa as IFileSystemAccess2; + val context = new GeneratorContext(); + context.setCancelIndicator(CancelIndicator.NullImpl); + try { + beforeGenerate(input, casted, context); + doGenerate(input, casted, context); + } finally { + afterGenerate(input, casted, context); + } + } + + def public void setRBAModelInBuilding(boolean value) { + sortValueGeneratorInBuilding.set(value); + rtModelUpdaterInBuilding.set(value); + constraintGeneratorInBuilding.set(value); + jsonGeneratorInBuilding.set(value); + } + + def public boolean isRBAModelInBuilding() { + if (sortValueGeneratorInBuilding.get().booleanValue) { + return true; + } + if (rtModelUpdaterInBuilding.get().booleanValue) { + return true; + } + if (constraintGeneratorInBuilding.get().booleanValue) { + return true; + } + if (jsonGeneratorInBuilding.get().booleanValue) { + return true; + } + return false; + } + + def public Set<OutputConfiguration> getRBAModelGeneratorOutputConfigurations() { + return newHashSet(IJSONGenerator.OUTPUT_CONFIGURATION); + } + +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/RBAModelGeneratorExtensions.xtend b/rba.tool.editor/src/rba/tool/editor/generator/RBAModelGeneratorExtensions.xtend new file mode 100644 index 0000000..8666e9b --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/RBAModelGeneratorExtensions.xtend @@ -0,0 +1,680 @@ +package rba.tool.editor.generator + +import java.util.HashMap +import java.util.Map +import org.eclipse.emf.ecore.EObject +import rba.core.AbstractProperty +import rba.core.AllocatedContent +import rba.core.AndOperator +import rba.core.Content +import rba.core.ContentSet +import rba.core.ContentValue +import rba.core.ExistsOperator +import rba.core.Expression +import rba.core.ForAllOperator +import rba.core.GetAllocatables +import rba.core.GetContentsList +import rba.core.GetProperty +import rba.core.IfActionOperator +import rba.core.IfStatement +import rba.core.ImpliesOperator +import rba.core.IntegerValue +import rba.core.IsActive +import rba.core.IsCanceled +import rba.core.IsDisappeared +import rba.core.IsEqualToOperator +import rba.core.IsGreaterThanEqualOperator +import rba.core.IsGreaterThanOperator +import rba.core.IsLowerThanEqualOperator +import rba.core.IsLowerThanOperator +import rba.core.IsOn +import rba.core.LambdaExpression +import rba.core.MaxValue +import rba.core.MinValue +import rba.core.NoneValue +import rba.core.NotOperator +import rba.core.ObjectCompare +import rba.core.ObjectReference +import rba.core.OffScene +import rba.core.OnScene +import rba.core.OrOperator +import rba.core.PreviousModifier +import rba.core.Scene +import rba.core.SetOfOperator +import rba.core.SetProperty +import rba.core.StandardValue +import rba.core.Variable +import rba.sound.AllInstanceOfSoundContent +import rba.sound.AllInstanceOfZone +import rba.sound.IsAttenuated +import rba.sound.IsMuted +import rba.sound.IsOutputted +import rba.sound.IsSounding +import rba.sound.OutputtingSound +import rba.sound.Zone +import rba.sound.ZoneSet +import rba.view.AllInstanceOfArea +import rba.view.AllInstanceOfViewContent +import rba.view.Area +import rba.view.AreaSet +import rba.view.DisplayingContent +import rba.view.IsDisplayed +import rba.view.IsHidden +import rba.view.IsVisible +import rba.core.ContentState +import rba.core.State + +class RBAModelGeneratorExtensions { + + public int operandIndex = 1; + + public Map<EObject, String> variableNames = new HashMap<EObject, String>(); + + def public compile(Expression e, String text) ''' + «e.compile(null, text, null)» + ''' + + def public compile(Expression e, LambdaExpression le, String text1, String text2) ''' + «IF e instanceof IsEqualToOperator » + «(e as IsEqualToOperator).compile(text1)» + «ELSEIF e instanceof IsGreaterThanOperator » + «(e as IsGreaterThanOperator).compile(text1)» + «ELSEIF e instanceof IsLowerThanOperator » + «(e as IsLowerThanOperator).compile(text1)» + «ELSEIF e instanceof IsGreaterThanEqualOperator » + «(e as IsGreaterThanEqualOperator).compile(text1)» + «ELSEIF e instanceof IsLowerThanEqualOperator » + «(e as IsLowerThanEqualOperator).compile(text1)» + «ELSEIF e instanceof AndOperator » + «(e as AndOperator).compile(text1)» + «ELSEIF e instanceof OrOperator» + «(e as OrOperator).compile(text1)» + «ELSEIF e instanceof NotOperator» + «(e as NotOperator).compile(text1)» + «ELSEIF e instanceof ImpliesOperator» + «(e as ImpliesOperator).compile(text1)» + «ELSEIF e instanceof IsActive» + «(e as IsActive).compile(text1)» + «ELSEIF e instanceof IsVisible» + «(e as IsVisible).compile(text1)» + «ELSEIF e instanceof GetAllocatables» + «(e as GetAllocatables).compile(le, text1, text2)» + «ELSEIF e instanceof IsDisplayed» + «(e as IsDisplayed).compile(text1)» + «ELSEIF e instanceof IsHidden» + «(e as IsHidden).compile(text1)» + «ELSEIF e instanceof DisplayingContent» + «(e as DisplayingContent).compile(le, text1, text2)» + «ELSEIF e instanceof AllocatedContent» + «(e as AllocatedContent).compile(le, text1, text2)» + «ELSEIF e instanceof GetContentsList» + «(e as GetContentsList).compile(le, text1, text2)» + «ELSEIF e instanceof ContentValue» + «(e as ContentValue).compile(le, text1, text2)» + «ELSEIF e instanceof ObjectReference» + «(e as ObjectReference).compile(le, text1, text2)» + «ELSEIF e instanceof PreviousModifier» + «(e as PreviousModifier).compile(text1)» + «ELSEIF e instanceof ObjectCompare» + «(e as ObjectCompare).compile(text1)» + «ELSEIF e instanceof ForAllOperator» + «(e as ForAllOperator).compile(text1)» + «ELSEIF e instanceof ExistsOperator» + «(e as ExistsOperator).compile(text1)» + «ELSEIF e instanceof AllInstanceOfArea» + «(e as AllInstanceOfArea).compile(le, text1, text2)» + «ELSEIF e instanceof AllInstanceOfViewContent» + «(e as AllInstanceOfViewContent).compile(le, text1, text2)» + «ELSEIF e instanceof AllInstanceOfZone» + «(e as AllInstanceOfZone).compile(le, text1, text2)» + «ELSEIF e instanceof AllInstanceOfSoundContent» + «(e as AllInstanceOfSoundContent).compile(le, text1, text2)» + «ELSEIF e instanceof SetOfOperator» + «(e as SetOfOperator).compile(le, text1, text2)» + «ELSEIF e instanceof IfStatement» + «(e as IfStatement).compile(le, text1, text2)» + «ELSEIF e instanceof IsOn» + «(e as IsOn).compile(text1)» + «ELSEIF e instanceof IsDisappeared» + «(e as IsDisappeared).compile(text1)» + «ELSEIF e instanceof IsCanceled» + «(e as IsCanceled).compile(text1)» + «ELSEIF e instanceof GetProperty» + «(e as GetProperty).compile(le, text1, text2)» + «ELSEIF e instanceof SetProperty» + «(e as SetProperty).compile(le, text1, text2)» + «ELSEIF e instanceof OffScene» + «(e as OffScene).compile(text1)» + «ELSEIF e instanceof OnScene» + «(e as OnScene).compile(text1)» + «ELSEIF e instanceof IsSounding» + «(e as IsSounding).compile(text1)» + «ELSEIF e instanceof IsOutputted» + «(e as IsOutputted).compile(text1)» + «ELSEIF e instanceof IsMuted» + «(e as IsMuted).compile(text1)» + «ELSEIF e instanceof OutputtingSound» + «(e as OutputtingSound).compile(le, text1, text2)» + «ELSEIF e instanceof IsAttenuated» + «(e as IsAttenuated).compile(text1)» + «ELSEIF e instanceof IfActionOperator» + «(e as IfActionOperator).compile(le, text1, text2)» + «ELSEIF e instanceof MaxValue» + «(e as MaxValue).compile(text1)» + «ELSEIF e instanceof MinValue» + «(e as MinValue).compile(text1)» + «ELSEIF e instanceof NoneValue» + «(e as NoneValue).compile(text1)» + «ELSEIF e instanceof StandardValue» + «(e as StandardValue).compile(text1)» + «ELSEIF e instanceof IntegerValue» + «(e as IntegerValue).compile(text1)» + «ENDIF» + ''' + + def public compile(IsEqualToOperator o, String addExpressionStatement) ''' + «var name = "isEqualToOperator_" + operandIndex++» + ARBIsEqualToOperator «name» = ArbFactory.eINSTANCE.createARBIsEqualToOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsGreaterThanOperator o, String addExpressionStatement) ''' + «var name = "isGreaterThanOperator_" + operandIndex++» + ARBIsGreaterThanOperator «name» = ArbFactory.eINSTANCE.createARBIsGreaterThanOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsLowerThanOperator o, String addExpressionStatement) ''' + «var name = "isLowerThanOperator_" + operandIndex++» + ARBIsLowerThanOperator «name» = ArbFactory.eINSTANCE.createARBIsLowerThanOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsGreaterThanEqualOperator o, String addExpressionStatement) ''' + «var name = "isGreaterThanEqualOperator_" + operandIndex++» + ARBIsGreaterThanEqualOperator «name» = ArbFactory.eINSTANCE.createARBIsGreaterThanEqualOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsLowerThanEqualOperator o, String addExpressionStatement) ''' + «var name = "isLowerThanEqualOperator_" + operandIndex++» + ARBIsLowerThanEqualOperator «name» = ArbFactory.eINSTANCE.createARBIsLowerThanEqualOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(AndOperator o, String addExpressionStatement) ''' + «var name = "andOperator_" + operandIndex++» + ARBAndOperator «name» = ArbFactory.eINSTANCE.createARBAndOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(OrOperator o, String addExpressionStatement) ''' + «var name = "orOperator_" + operandIndex++» + ARBOrOperator «name» = ArbFactory.eINSTANCE.createARBOrOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(NotOperator o, String addExpressionStatement) ''' + «var name = "notOperator_" + operandIndex++» + ARBNotOperator «name» = ArbFactory.eINSTANCE.createARBNotOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(ImpliesOperator o, String addExpressionStatement) ''' + «var name = "impliesOperator_" + operandIndex++» + ARBImpliesOperator «name» = ArbFactory.eINSTANCE.createARBImpliesOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(ObjectCompare o, String addExpressionStatement) ''' + «var name = "objectCompair_" + operandIndex++» + ARBObjectCompare «name» = ArbFactory.eINSTANCE.createARBObjectCompare(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsActive o, String addExpressionStatement) ''' + «var name = "isActive_" + operandIndex++» + ARBIsActive «name» = ArbFactory.eINSTANCE.createARBIsActive(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsVisible o, String addExpressionStatement) ''' + «var name = "isVisible_" + operandIndex++» + ARBIsVisible «name» = ArbFactory.eINSTANCE.createARBIsVisible(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(GetAllocatables o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "getAllocatables_" + operandIndex++» + ARBGetAllocatables «name» = ArbFactory.eINSTANCE.createARBGetAllocatables(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsDisplayed o, String addExpressionStatement) ''' + «var name = "isDisplayed_" + operandIndex++» + ARBIsDisplayed «name» = ArbFactory.eINSTANCE.createARBIsDisplayed(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsHidden o, String addExpressionStatement) ''' + «var name = "isHidden_" + operandIndex++» + ARBIsHidden «name» = ArbFactory.eINSTANCE.createARBIsHidden(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(DisplayingContent o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "displayingContent_" + operandIndex++» + ARBDisplayingContent «name» = ArbFactory.eINSTANCE.createARBDisplayingContent(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(AllocatedContent o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "allocatedContent_" + operandIndex++» + ARBAllocatedContent «name» = ArbFactory.eINSTANCE.createARBAllocatedContent(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(GetContentsList o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "getContentsList_" + operandIndex++» + ARBGetContentsList «name» = ArbFactory.eINSTANCE.createARBGetContentsList(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(ContentValue o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "contentValue_" + operandIndex++» + ARBContentValue «name» = ArbFactory.eINSTANCE.createARBContentValue(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + public static final String DummyIndicateCharacter = "|"; //$NON-NLS-1$ + + def public compile(ObjectReference o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "objectReference_" + operandIndex++» + ARBObjectReference «name» = ArbFactory.eINSTANCE.createARBObjectReference(); + «name».setRefObject(«IF o.refObject instanceof Scene »model.getScene("«o.refObject.name»"));«ELSEIF o.refObject instanceof ContentState »model.getContentState("«(o.refObject as ContentState).owner.name»", "«o.refObject.name»")); + «ELSEIF o.refObject instanceof AbstractProperty »model.getProperty("«(o.refObject as AbstractProperty).owner.name»", "«o.refObject.name»"));«ELSEIF o.refObject instanceof Zone »model.getAllocatable("«o.refObject.name»"));«ELSEIF o.refObject instanceof ZoneSet»model.getAllocatableSet("«o.refObject.name»"));«ELSEIF o.refObject instanceof Area »model.getAllocatable("«o.refObject.name»"));«ELSEIF o.refObject instanceof Content»model.getContent("«o.refObject.name»"));«ELSEIF o.refObject instanceof AreaSet»model.getAllocatableSet("«o.refObject.name»"));«ELSEIF o.refObject instanceof ContentSet»model.getContentSet("«o.refObject.name»"));«ELSEIF o.refObject instanceof Variable»«IF variableNames.containsKey(o.refObject)»«variableNames.get(o.refObject)»«ELSE»null«ENDIF»);«ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(PreviousModifier o, String addExpressionStatement) ''' + «var name = "previousModifier_" + operandIndex++» + ARBPreviousModifier «name» = ArbFactory.eINSTANCE.createARBPreviousModifier(); + «IF o.objReference !== null» + «o.objReference.compile(name + ".setObjReference")» + «ELSE» + «name».setObjReference(null); + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(ForAllOperator o, String addExpressionStatement) ''' + «var name = "forAllOperator_" + operandIndex++» + ARBForAllOperator «name» = ArbFactory.eINSTANCE.createARBForAllOperator(); + «IF o.operand !== null && o.operand.size > 0 && o.lambda !== null» + «(o.operand.get(0)).compile(o.lambda, name + ".getOperands().add", name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(ExistsOperator o, String addExpressionStatement) ''' + «var name = "existsOperator_" + operandIndex++» + ARBExistsOperator «name» = ArbFactory.eINSTANCE.createARBExistsOperator(); + «IF o.operand !== null && o.operand.size > 0 && o.lambda !== null» + «(o.operand.get(0)).compile(o.lambda, name + ".getOperands().add", name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(LambdaExpression o, String addExpressionStatement, String refContextObjectName, String setExpressionStatement) ''' + «var name = "lambdaExpression_" + operandIndex++» + ARBLambdaExpression «name» = ArbFactory.eINSTANCE.createARBLambdaExpression(); + «name».setContext(«refContextObjectName»); + «IF o.x !== null && o.bodyText !== null» + «(o.x).compile(name + ".setX", setExpressionStatement)» + «(o.bodyText).compile(name + ".setBodyText")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(Variable v, String addExpressionStatement, String refExpressionObjectName) ''' + «var name = "variable_" + operandIndex++» + «variableNames.put(v, name)» + ARBVariable «name» = ArbFactory.eINSTANCE.createARBVariable(); + «name».setDescription(«IF v.description === null»""«ELSEIF v.description.empty»""«ELSE»«v.description»«ENDIF»); + «name».setName("«v.name»"); + «name».setType(ARB«v.expressionType.class.simpleName».«v.expressionType.getName»); + «name».setExpression(«refExpressionObjectName»); + «addExpressionStatement»(«name»); + ''' + + def public compile(AllInstanceOfArea o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "allInstanceOfArea_" + operandIndex++» + ARBAllInstanceOfArea «name» = ArbFactory.eINSTANCE.createARBAllInstanceOfArea(); + «name».setRefObject(model.getAllArea()); + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(AllInstanceOfViewContent o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "allInstanceOfViewContent_" + operandIndex++» + ARBAllInstanceOfContent «name» = ArbFactory.eINSTANCE.createARBAllInstanceOfContent(); + «name».setRefObject(model.getAllViewContent()); + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(AllInstanceOfZone o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "allInstanceOfZone_" + operandIndex++» + ARBAllInstanceOfZone «name» = ArbFactory.eINSTANCE.createARBAllInstanceOfZone(); + «name».setRefObject(model.getAllZone()); + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(AllInstanceOfSoundContent o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "allInstanceOfSoundContent_" + operandIndex++» + ARBAllInstanceOfSoundContent «name» = ArbFactory.eINSTANCE.createARBAllInstanceOfSoundContent(); + «name».setRefObject(model.getAllSoundContent()); + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(SetOfOperator o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "setOfOperator_" + operandIndex++» + ARBSetOfOperator «name» = ArbFactory.eINSTANCE.createARBSetOfOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IfStatement o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "ifStatement_" + operandIndex++» + ARBIfStatement «name» = ArbFactory.eINSTANCE.createARBIfStatement(); + «IF o.condition !== null» + «(o.condition).compile(name + ".setCondition")» + «ENDIF» + «IF o.thenExpression !== null» + «(o.thenExpression).compile(name + ".setThenExpression")» + «ENDIF» + «IF o.elseExpression !== null» + «(o.elseExpression).compile(name + ".setElseExpression")» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsOn o, String addExpressionStatement) ''' + «var name = "isOn_" + operandIndex++» + ARBIsOn «name» = ArbFactory.eINSTANCE.createARBIsOn(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsDisappeared o, String addExpressionStatement) ''' + «var name = "isDisappeared_" + operandIndex++» + ARBIsDisappeared «name» = ArbFactory.eINSTANCE.createARBIsDisappeared(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsCanceled o, String addExpressionStatement) ''' + «var name = "isCanceled_" + operandIndex++» + ARBIsCanceled «name» = ArbFactory.eINSTANCE.createARBIsCanceled(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(GetProperty o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "getProperty_" + operandIndex++» + ARBGetProperty «name» = ArbFactory.eINSTANCE.createARBGetProperty(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(SetProperty o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "setProperty_" + operandIndex++» + ARBSetProperty «name» = ArbFactory.eINSTANCE.createARBSetProperty(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(OffScene o, String addExpressionStatement) ''' + «var name = "offScene_" + operandIndex++» + ARBOffScene «name» = ArbFactory.eINSTANCE.createARBOffScene(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(OnScene o, String addExpressionStatement) ''' + «var name = "onScene_" + operandIndex++» + ARBOnScene «name» = ArbFactory.eINSTANCE.createARBOnScene(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsSounding o, String addExpressionStatement) ''' + «var name = "isSounding_" + operandIndex++» + ARBIsSounding «name» = ArbFactory.eINSTANCE.createARBIsSounding(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsOutputted o, String addExpressionStatement) ''' + «var name = "isOutputted_" + operandIndex++» + ARBIsOutputted «name» = ArbFactory.eINSTANCE.createARBIsOutputted(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsMuted o, String addExpressionStatement) ''' + «var name = "isMuted_" + operandIndex++» + ARBIsMuted «name» = ArbFactory.eINSTANCE.createARBIsMuted(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(OutputtingSound o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "outputtingSound_" + operandIndex++» + ARBOutputtingSound «name» = ArbFactory.eINSTANCE.createARBOutputtingSound(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IsAttenuated o, String addExpressionStatement) ''' + «var name = "isAttenuated_" + operandIndex++» + ARBIsAttenuated «name» = ArbFactory.eINSTANCE.createARBIsAttenuated(); + «IF o.operand !== null && o.operand.size > 0» + «(o.operand.get(0)).compile(name + ".getOperands().add")» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(IfActionOperator o, LambdaExpression le, String addExpressionStatement, String parentName) ''' + «var name = "ifActionOperator_" + operandIndex++» + ARBIfActionOperator «name» = ArbFactory.eINSTANCE.createARBIfActionOperator(); + «IF o.operand !== null && o.operand.size > 0» + «FOR op : o.operand» + «op.compile(name + ".getOperands().add")» + «ENDFOR» + «ENDIF» + «IF le !== null && parentName !== null && !parentName.empty» + «le.compile(parentName + ".setLambda", parentName, name)» + «ENDIF» + «addExpressionStatement»(«name»); + ''' + + def public compile(MaxValue o, String addExpressionStatement) ''' + «var name = "maxValue_" + operandIndex++» + ARBMaxValue «name» = ArbFactory.eINSTANCE.createARBMaxValue(); + «addExpressionStatement»(«name»); + ''' + + def public compile(MinValue o, String addExpressionStatement) ''' + «var name = "minValue_" + operandIndex++» + ARBMinValue «name» = ArbFactory.eINSTANCE.createARBMinValue(); + «addExpressionStatement»(«name»); + ''' + + def public compile(NoneValue o, String addExpressionStatement) ''' + «var name = "noneValue_" + operandIndex++» + ARBNoneValue «name» = ArbFactory.eINSTANCE.createARBNoneValue(); + «addExpressionStatement»(«name»); + ''' + + def public compile(StandardValue o, String addExpressionStatement) ''' + «var name = "standardValue_" + operandIndex++» + ARBStandardValue «name» = ArbFactory.eINSTANCE.createARBStandardValue(); + «addExpressionStatement»(«name»); + ''' + + def public compile(IntegerValue o, String addExpressionStatement) ''' + «var name = "integerValue_" + operandIndex++» + ARBIntegerValue «name» = ArbFactory.eINSTANCE.createARBIntegerValue(); + «name».setValue(«o.value»); + «addExpressionStatement»(«name»); + ''' +}
\ No newline at end of file diff --git a/rba.tool.editor/src/rba/tool/editor/generator/json/AbstractJSONGenerator.xtend b/rba.tool.editor/src/rba/tool/editor/generator/json/AbstractJSONGenerator.xtend new file mode 100644 index 0000000..5b5715e --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/json/AbstractJSONGenerator.xtend @@ -0,0 +1,52 @@ +package rba.tool.editor.generator.json + +import java.util.List +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.emf.ecore.resource.ResourceSet +import org.eclipse.emf.workspace.util.WorkspaceSynchronizer +import org.eclipse.xtext.generator.AbstractFileSystemAccess +import org.eclipse.xtext.generator.AbstractGenerator +import org.eclipse.xtext.generator.IFileSystemAccess2 +import org.eclipse.xtext.generator.IGeneratorContext +import rba.tool.editor.model.manager.ResourceManager +import rba.view.Display + +abstract class AbstractJSONGenerator extends AbstractGenerator implements IJSONGenerator { + + override doGenerate(Resource input, IFileSystemAccess2 fsa, IGeneratorContext context) { + doGenerate(input.resourceSet, fsa, context); + } + + override beforeGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + } + + override afterGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + } + + override doGenerate(ResourceSet resourceSet, IFileSystemAccess2 fsa, IGeneratorContext context) { + if (resourceSet.resources.empty) { + return; + } + val resource = resourceSet.resources.get(0); + val file = WorkspaceSynchronizer.getFile(resource); + if (!file.exists) { + return; + } + + val project = file.project; + if (project === null) { + return; + } + + if (!(fsa instanceof AbstractFileSystemAccess)) { + return; + } + + val allDisplays = ResourceManager.INSTANCE.getRbaDisplays(resourceSet); + + fsa.generateFile("data.js", OUTPUT_CONFIGURATION.name, createJSONFile(allDisplays)); + } + + def abstract public String createJSONFile(List<Display> displays); + +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/json/IJSONGenerator.xtend b/rba.tool.editor/src/rba/tool/editor/generator/json/IJSONGenerator.xtend new file mode 100644 index 0000000..e65c130 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/json/IJSONGenerator.xtend @@ -0,0 +1,18 @@ +package rba.tool.editor.generator.json + +import org.eclipse.emf.ecore.resource.ResourceSet +import org.eclipse.xtext.generator.IFileSystemAccess2 +import org.eclipse.xtext.generator.IGenerator2 +import org.eclipse.xtext.generator.IGeneratorContext +import org.eclipse.xtext.generator.OutputConfiguration + +interface IJSONGenerator extends IGenerator2 { + + static OutputConfiguration OUTPUT_CONFIGURATION = new JSONGeneratorOutputConfiguration(); + + def void doGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); + + def void beforeGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); + + def void afterGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/json/JSONGeneratorOutputConfiguration.xtend b/rba.tool.editor/src/rba/tool/editor/generator/json/JSONGeneratorOutputConfiguration.xtend new file mode 100644 index 0000000..fc6a73c --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/json/JSONGeneratorOutputConfiguration.xtend @@ -0,0 +1,18 @@ +package rba.tool.editor.generator.json + +import org.eclipse.xtext.generator.OutputConfiguration + +class JSONGeneratorOutputConfiguration extends OutputConfiguration { + + new() { + super("RBAMODEL_JSONGENERATOR_OUTPUT"); + setDescription("Output Folder"); + setOutputDirectory("./.RBATool/graphicalview/data"); + setOverrideExistingResources(true); + setCreateOutputDirectory(true); + setCleanUpDerivedResources(true); + setSetDerivedProperty(true); + setKeepLocalHistory(true); + } + +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/rtmodel/AbstractRTModelUpdater.xtend b/rba.tool.editor/src/rba/tool/editor/generator/rtmodel/AbstractRTModelUpdater.xtend new file mode 100644 index 0000000..4435813 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/rtmodel/AbstractRTModelUpdater.xtend @@ -0,0 +1,23 @@ +package rba.tool.editor.generator.rtmodel + +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.emf.ecore.resource.ResourceSet +import org.eclipse.xtext.generator.AbstractGenerator +import org.eclipse.xtext.generator.IFileSystemAccess2 +import org.eclipse.xtext.generator.IGeneratorContext + +abstract class AbstractRTModelUpdater extends AbstractGenerator implements IRTModelUpdater { + + override doGenerate(Resource input, IFileSystemAccess2 fsa, IGeneratorContext context) { + doGenerate(input.resourceSet, fsa, context); + } + + override beforeGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + } + + override afterGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + } + +// override doGenerate(ResourceSet resourceSet, IFileSystemAccess2 fsa, IGeneratorContext context) { +// } +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/rtmodel/IRTModelUpdater.xtend b/rba.tool.editor/src/rba/tool/editor/generator/rtmodel/IRTModelUpdater.xtend new file mode 100644 index 0000000..010e508 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/rtmodel/IRTModelUpdater.xtend @@ -0,0 +1,15 @@ +package rba.tool.editor.generator.rtmodel + +import org.eclipse.emf.ecore.resource.ResourceSet +import org.eclipse.xtext.generator.IFileSystemAccess2 +import org.eclipse.xtext.generator.IGenerator2 +import org.eclipse.xtext.generator.IGeneratorContext + +interface IRTModelUpdater extends IGenerator2 { + + def void doGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); + + def void beforeGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); + + def void afterGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintCodeGenerationSupporter.java b/rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintCodeGenerationSupporter.java new file mode 100644 index 0000000..b587cc7 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintCodeGenerationSupporter.java @@ -0,0 +1,1599 @@ +package rba.tool.editor.generator.z3; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import org.eclipse.emf.common.util.EList; +import org.eclipse.emf.ecore.EObject; + +import rba.core.AbstractAllocatable; +import rba.core.AbstractConstraint; +import rba.core.AbstractContent; +import rba.core.ActiveContents; +import rba.core.Allocatable; +import rba.core.AllocatableSet; +import rba.core.AllocatedContent; +import rba.core.AndOperator; +import rba.core.ComplexExpression; +import rba.core.Constraint; +import rba.core.Content; +import rba.core.ContentSet; +import rba.core.ContentValue; +import rba.core.ExistsOperator; +import rba.core.Expression; +import rba.core.ExpressionType; +import rba.core.ForAllOperator; +import rba.core.GetAllocatables; +import rba.core.GetContentsList; +import rba.core.GetProperty; +import rba.core.HasBeenDisplayed; +import rba.core.HasComeEarlierThan; +import rba.core.HasComeLaterThan; +import rba.core.IfStatement; +import rba.core.ImpliesOperator; +import rba.core.IntegerProperty; +import rba.core.IntegerValue; +import rba.core.IsActive; +import rba.core.IsCanceled; +import rba.core.IsDisappeared; +import rba.core.IsEqualToOperator; +import rba.core.IsGreaterThanEqualOperator; +import rba.core.IsGreaterThanOperator; +import rba.core.IsLowerThanEqualOperator; +import rba.core.IsLowerThanOperator; +import rba.core.IsOn; +import rba.core.LambdaContext; +import rba.core.LambdaExpression; +import rba.core.NotOperator; +import rba.core.ObjectCompare; +import rba.core.ObjectReference; +import rba.core.OrOperator; +import rba.core.PreviousModifier; +import rba.core.RuleObject; +import rba.core.Scene; +import rba.core.SetOfOperator; +import rba.core.SugarExpression; +import rba.core.Variable; +import rba.sound.AllInstanceOfSoundContent; +import rba.sound.AllInstanceOfZone; +import rba.sound.IsAttenuated; +import rba.sound.IsMuted; +import rba.sound.IsOutputted; +import rba.sound.IsSounding; +import rba.sound.OutputtingSound; +import rba.sound.SoundContent; +import rba.sound.SoundContentSet; +import rba.sound.Zone; +import rba.sound.ZoneSet; +import rba.view.AllInstanceOfArea; +import rba.view.AllInstanceOfViewContent; +import rba.view.Area; +import rba.view.AreaSet; +import rba.view.DisplayingContent; +import rba.view.IsDisplayed; +import rba.view.IsHidden; +import rba.view.IsVisible; +import rba.view.ViewContent; +import rba.view.ViewContentSet; + +public class ConstraintCodeGenerationSupporter implements GeneratorConstants { + + static ConstraintCodeTemplate template = new ConstraintCodeTemplate(); + + private List<Allocatable> allocatableList = new ArrayList<Allocatable>(); + + private int areaListEndIndex; + + private List<Content> contentList = new ArrayList<Content>(); + + private int viewContentListEndIndex; + + private int soundContentListEndIndex; + + private List<ContentSet> contentSetList = new ArrayList<ContentSet>(); + + private int viewContentSetListEndIndex; + + private List<AllocatableSet> allocatableSetList = new ArrayList<AllocatableSet>(); + + private int areaSetListEndIndex; + + private List<Variable> variableList; + + private List<Constraint> constraintList; + + private List<Scene> sceneList; + + private List<SetOfOperator> setOfOpeList; + + private Map<Variable, String> variableNameMap = new HashMap<Variable, String>(); + + private Map<AllocatableSet, String> allocatableSetNameMap = new HashMap<AllocatableSet, String>(); + + private Map<ContentSet, String> contentSetNameMap = new HashMap<ContentSet, String>(); + + private Map<String, String> SetOfNameMap = new HashMap<String, String>(); + + private List<ImpliseConstraintInfo> impliseMethodList = new ArrayList<ImpliseConstraintInfo>(); + + private List<ImpliseConstraintInfo> postImpliseMethodList = new ArrayList<ImpliseConstraintInfo>(); + + public String generate(List<ViewContent> viewContentList, List<SoundContent> soundContentList, List<Area> areaList, List<Zone> zoneList, + List<ViewContentSet> viewContentSetList, List<SoundContentSet> soundContentSetList, List<AreaSet> areaSetList, List<ZoneSet> zoneSetList, List<Variable> variables, + List<Constraint> constraints, List<Scene> scenes, List<SetOfOperator> setOfOperators) { + this.variableList = variables; + this.constraintList = constraints; + this.sceneList = scenes; + this.setOfOpeList = setOfOperators; + + variableNameMap.clear(); + allocatableSetNameMap.clear(); + contentSetNameMap.clear(); + SetOfNameMap.clear(); + impliseMethodList.clear(); + postImpliseMethodList.clear(); + + allocatableList.clear(); + contentList.clear(); + allocatableSetList.clear(); + contentSetList.clear(); + + areaListEndIndex = areaList.size(); + allocatableList.addAll(areaList); + allocatableList.addAll(zoneList); + + viewContentListEndIndex = viewContentList.size(); + soundContentListEndIndex = viewContentListEndIndex + soundContentList.size(); + contentList.addAll(viewContentList); + contentList.addAll(soundContentList); + + areaSetListEndIndex = areaSetList.size(); + allocatableSetList.addAll(areaSetList); + allocatableSetList.addAll(zoneSetList); + + viewContentSetListEndIndex = viewContentSetList.size(); + contentSetList.addAll(viewContentSetList); + contentSetList.addAll(soundContentSetList); + + StringBuilder setupList_Adding = new StringBuilder(); + StringBuilder init_Adding = new StringBuilder(); + StringBuilder fieldVariableAdding = new StringBuilder(); + StringBuilder allocatable_content_sizeAdding = new StringBuilder(); + + StringBuilder constraintList_Adding = new StringBuilder(); + StringBuilder impliesConstraintMethodList_Adding = new StringBuilder(); + StringBuilder impliesConstraintMethodCallList_Adding = new StringBuilder(); + + setAllocatableContext(allocatableList.subList(0, areaListEndIndex), init_Adding, "Area"); + setAllocatableContext(allocatableList.subList(areaListEndIndex, allocatableList.size()), init_Adding, "Zone"); + setContetContext(contentList.subList(0, viewContentListEndIndex), init_Adding, "ViewContent"); + setContetContext(contentList.subList(viewContentListEndIndex, soundContentListEndIndex), init_Adding, "SoundContent"); + + setAllocatableSetContext(AREASET_VAR_NAME, allocatableSetList.subList(0, areaSetListEndIndex), init_Adding, fieldVariableAdding, setupList_Adding); + setAllocatableSetContext(ZONESET_VAR_NAME, allocatableSetList.subList(areaSetListEndIndex, allocatableSetList.size()), init_Adding, fieldVariableAdding, setupList_Adding); + setContentSetContext(VIEW_CONTENTSET_VAR_NAME, contentSetList.subList(0, viewContentSetListEndIndex), init_Adding, fieldVariableAdding, setupList_Adding); + setContentSetContext(SOUND_CONTENTSET_VAR_NAME, contentSetList.subList(viewContentSetListEndIndex, contentSetList.size()), init_Adding, fieldVariableAdding, + setupList_Adding); + + allocatable_content_sizeAdding.append(_8SPACES + "allocatableSize = ctx.mkInt(" + allocatableList.size() + ");" + NL); + allocatable_content_sizeAdding.append(_8SPACES + "contentSize = ctx.mkInt(" + contentList.size() + ");"); + + for (int i = 0; i < variableList.size(); i++) { + Variable variable = variableList.get(i); + String varName = VARIABLE_VAR_NAME + (i + 1); + String define = String.format(VARIABLE_DEFINE, varName); + + constraintList_Adding.append(_8SPACES + VARIABLE_CMT + variable.getName() + NL); + constraintList_Adding.append(_8SPACES + define + NL); + constraintList_Adding.append(_8SPACES + varName + ARRAY_TOP + String.format(SET_VARIABLE_VALUE, variable.getName()) + NL); + + variableNameMap.put(variable, varName); + } + + for (int i = 0; i < setOfOpeList.size(); i++) { + SetOfOperator setOfOp = setOfOpeList.get(i); + + String varName = SETOF_OP_VAR_NAME + (i + 1); + String expressionText = setOfOp.getExpressionText(); + String string = SetOfNameMap.get(expressionText); + if (string != null) { + continue; + } + SetOfNameMap.put(expressionText, varName); + + String label = STR_QUOTE + CONSTRAINT_PREFIX + varName + STR_QUOTE; + String storeStr = getStoreExpr(setOfOp); + + fieldVariableAdding.append(_4SPACES + ARRAY_EXPR_SORT + varName + END + NL); + + setupList_Adding + .append(_8SPACES + varName + EQUAL + EX_CTX_MK_ARRAY_CONST + OPEN + STR_QUOTE + varName + STR_QUOTE + COMMA + INT_TYPE + COMMA + BOOL_TYPE + CLOSE + END + NL); + + init_Adding.append(_8SPACES + SL_COMMENT + varName + EQUAL + expressionText + NL); + init_Adding.append(_8SPACES + CONSTR_LIST_ADD + OPEN + EX_CTX_MK_EQ + OPEN + varName + COMMA + storeStr + CLOSE + CLOSE + END + NL); + init_Adding.append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + label + CLOSE + CLOSE + END + NL); + } + + constraintList_Adding.append(NL); + + for (int i = 0; i < constraintList.size(); i++) { + Constraint constraint = constraintList.get(i); + if (constraint.getExpression() == null) { + continue; + } + + setConstraintList(constraintList_Adding, impliesConstraintMethodList_Adding, constraint, constraint.isRuntime(), i); + } + + for (ImpliseConstraintInfo info : impliseMethodList) { + setImpliesConstraintMethod(impliesConstraintMethodCallList_Adding, info); + } + + String invarianceConstraintStr = getInvarianceConstraintStr(false); + String invariancePreConstraintStr = getInvarianceConstraintStr(true); + + template.allocatable_content_set_code = fieldVariableAdding.toString(); + template.allocatable_content_size_code = allocatable_content_sizeAdding.toString(); + template.setup_code = setupList_Adding.toString(); + template.init_code = init_Adding.toString(); + template.constraints_code = constraintList_Adding.toString(); + template.implies_constraints_call_code = impliesConstraintMethodCallList_Adding.toString(); + template.implies_constraints_method_code = impliesConstraintMethodList_Adding.toString(); + template.invariance_constr_code = invarianceConstraintStr; + template.invariance_pre_constr_code = invariancePreConstraintStr; + + return template.getCompleteCode(); + } + + private void setAllocatableContext(List<Allocatable> list, StringBuilder init_Adding, String elementId) { + if (list.isEmpty()) { + return; + } + + for (int i = 0; i < list.size(); i++) { + Allocatable area = list.get(i); + + String contents = getContents(area); + String storeStr = getStoreExpr(area); + + int index = allocatableList.indexOf(area); + + init_Adding.append(_8SPACES + SL_COMMENT + area.getName() + " = { " + contents + " }" + NL); + + String selectLeft = EX_CTX_MK_SELECT + OPEN + OP_CONTENTS_LIST + COMMA + EX_CTX_MK_INT + OPEN + (index + 1) + CLOSE + CLOSE; + init_Adding.append(_8SPACES + CONSTR_LIST_ADD + OPEN + EX_CTX_MK_EQ + OPEN + selectLeft + COMMA + storeStr + CLOSE + CLOSE + END + NL); + String labelContentList = STR_QUOTE + CONSTRAINT_PREFIX + area.getName() + DOT + OP_CONTENTS_LIST + STR_QUOTE; + init_Adding.append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + labelContentList + CLOSE + CLOSE + END + NL); + } + init_Adding.append(NL); + } + + private void setContetContext(List<Content> list, StringBuilder init_Adding, String elementId) { + if (list.isEmpty()) { + return; + } + + for (int i = 0; i < list.size(); i++) { + Content content = list.get(i); + + String allocatable = getAllocatables(content); + String storeStr = getStoreExpr(content); + + int index = contentList.indexOf(content); + + init_Adding.append(_8SPACES + SL_COMMENT + content.getName() + " = { " + allocatable + " }" + NL); + + String selectLeft = EX_CTX_MK_SELECT + OPEN + OP_ALLOCATABLE + COMMA + EX_CTX_MK_INT + OPEN + (index + 1) + CLOSE + CLOSE; + init_Adding.append(_8SPACES + CONSTR_LIST_ADD + OPEN + EX_CTX_MK_EQ + OPEN + selectLeft + COMMA + storeStr + CLOSE + CLOSE + END + NL); + String labelContentList = STR_QUOTE + CONSTRAINT_PREFIX + content.getName() + DOT + OP_ALLOCATABLE + STR_QUOTE; + init_Adding.append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + labelContentList + CLOSE + CLOSE + END + NL); + } + init_Adding.append(NL); + } + + private void setAllocatableSetContext(String name, List<AllocatableSet> list, StringBuilder init_Adding, StringBuilder fieldVariableAdding, StringBuilder setupList_Adding) { + if (list.isEmpty()) { + return; + } + + for (int i = 0; i < list.size(); i++) { + AllocatableSet set = list.get(i); + String varName = name + (i + 1); + String label = STR_QUOTE + CONSTRAINT_PREFIX + set.getName() + STR_QUOTE; + String areas = getAreas(set); + String storeStr = getStoreExpr(set); + + fieldVariableAdding.append(_4SPACES + ARRAY_EXPR_SORT + varName + END + NL); + + setupList_Adding + .append(_8SPACES + varName + EQUAL + EX_CTX_MK_ARRAY_CONST + OPEN + STR_QUOTE + varName + STR_QUOTE + COMMA + INT_TYPE + COMMA + BOOL_TYPE + CLOSE + END + NL); + + init_Adding.append(_8SPACES + SL_COMMENT + set.getName() + " = { " + areas + " }" + NL); + init_Adding.append(_8SPACES + CONSTR_LIST_ADD + OPEN + EX_CTX_MK_EQ + OPEN + varName + COMMA + storeStr + CLOSE + CLOSE + END + NL); + init_Adding.append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + label + CLOSE + CLOSE + END + NL); + + allocatableSetNameMap.put(set, varName); + } + setupList_Adding.append(NL); + init_Adding.append(NL); + } + + private void setContentSetContext(String name, List<ContentSet> list, StringBuilder init_Adding, StringBuilder fieldVariableAdding, StringBuilder setupList_Adding) { + if (list.isEmpty()) { + return; + } + + for (int i = 0; i < list.size(); i++) { + ContentSet contentSet = list.get(i); + String varName = name + (i + 1); + String label = STR_QUOTE + CONSTRAINT_PREFIX + contentSet.getName() + STR_QUOTE; + String contents = getContents(contentSet); + String storeStr = getStoreExpr(contentSet); + + fieldVariableAdding.append(_4SPACES + ARRAY_EXPR_SORT + varName + END + NL); + + setupList_Adding + .append(_8SPACES + varName + EQUAL + EX_CTX_MK_ARRAY_CONST + OPEN + STR_QUOTE + varName + STR_QUOTE + COMMA + INT_TYPE + COMMA + BOOL_TYPE + CLOSE + END + NL); + + init_Adding.append(_8SPACES + SL_COMMENT + contentSet.getName() + " = { " + contents + " }" + NL); + init_Adding.append(_8SPACES + CONSTR_LIST_ADD + OPEN + EX_CTX_MK_EQ + OPEN + varName + COMMA + storeStr + CLOSE + CLOSE + END + NL); + init_Adding.append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + label + CLOSE + CLOSE + END + NL); + + contentSetNameMap.put(contentSet, varName); + } + init_Adding.append(NL); + } + + private void setConstraintList(StringBuilder constraintList_Adding, StringBuilder impliesConstraintMethodList_Adding, AbstractConstraint constraint, boolean runtime, + int index) { + + String label = STR_QUOTE + NUMBER + String.valueOf(index + 1) + ":" + constraint.getName() + STR_QUOTE; + String expressionText = constraint.getExpression().getExpressionText(); + constraintList_Adding.append(_8SPACES + SL_COMMENT + expressionText + NL); + String constraintContextString = ""; + + try { + constraintContextString = getContextString(constraint.getExpression()); + } catch (Exception e) { + constraintList_Adding.append(NL); + e.printStackTrace(); + return; + } + + Expression targetExpression = constraint.getExpression() instanceof ComplexExpression ? ((ComplexExpression)constraint.getExpression()).getOtherExpression() : constraint.getExpression(); + + if (isBoolOperator(targetExpression)) { + constraintContextString = EX_BOOL_EXPR + constraintContextString; + } + + String indent = ""; + if (!runtime) { + indent = _4SPACES; + constraintList_Adding.append(_8SPACES + IF_OFFLINE + NL); + } + constraintList_Adding.append(indent + _8SPACES + CONSTR_LIST_ADD + OPEN + constraintContextString + CLOSE + END + NL); + constraintList_Adding.append(indent + _8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + label + CLOSE + CLOSE + END + NL); + if (!runtime) { + constraintList_Adding.append(_8SPACES + BLOCK_CLOSE + NL); + } + constraintList_Adding.append(NL); + + if (isImplieseOperator(targetExpression)) { + impliesConstraintMethodList_Adding.append(getimpliesConstraintMethodsStr(constraint, index)); + } + } + + private void setImpliesConstraintMethod(StringBuilder impliesConstraintMethodCallList_Adding, ImpliseConstraintInfo info) { + int index = info.getIndex() + 1; + String indent = ""; + if (!info.isRuntime()) { + indent = _4SPACES; + impliesConstraintMethodCallList_Adding.append(_8SPACES + IF_OFFLINE + NL); + } + String methodName = info.getMethodName(); + + impliesConstraintMethodCallList_Adding.append(indent + _8SPACES + String.format(IMPLIES_CONSTRAINT_METHOD_DETAIL1, index) + methodName + END + NL); + impliesConstraintMethodCallList_Adding.append(indent + _8SPACES + String.format(IMPLIES_CONSTRAINT_METHOD_DETAIL2, index, index) + NL); + impliesConstraintMethodCallList_Adding + .append(indent + _4SPACES + _8SPACES + String.format(IMPLIES_CONSTRAINT_METHOD_DETAIL3, index, info.getConstraint().getName(), index) + END + NL); + impliesConstraintMethodCallList_Adding.append(indent + _4SPACES + _8SPACES + String.format(IMPLIES_CONSTRAINT_METHOD_DETAIL4, index) + NL); + impliesConstraintMethodCallList_Adding.append(indent + _8SPACES + _8SPACES + IMPLIES_CONSTRAINT_METHOD_DETAIL5 + END + NL); + impliesConstraintMethodCallList_Adding.append(indent + _4SPACES + _8SPACES + BLOCK_CLOSE + NL); + impliesConstraintMethodCallList_Adding.append(indent + _8SPACES + BLOCK_CLOSE + NL); + if (!info.isRuntime()) { + impliesConstraintMethodCallList_Adding.append(_8SPACES + BLOCK_CLOSE + NL); + } + impliesConstraintMethodCallList_Adding.append(NL); + } + + private String getimpliesConstraintMethodsStr(AbstractConstraint constraint, int index) { + StringBuilder methodsCommentList_Adding = new StringBuilder(); + StringBuilder constraintList_Adding = new StringBuilder(); + + Expression targetExpression = constraint.getExpression() instanceof ComplexExpression ? ((ComplexExpression)constraint.getExpression()).getOtherExpression() : constraint.getExpression(); + Expression leftExpression = ((ImpliesOperator) targetExpression).getOperand().get(0); + + ImpliseConstraintInfo info = new ImpliseConstraintInfo(); + info.setIndex(index); + info.setConstraint(constraint); + String methodName = ""; + String allConstMethodName = ""; + + if (constraint instanceof Constraint) { + // method name + methodName = String.format(IMPLIES_CONSTRAINT_METHOD_NAME, (index + 1)); + allConstMethodName = "setAllConstraintContext"; + info.setMethodName(methodName); + impliseMethodList.add(info); + } + + // comment + methodsCommentList_Adding.append(_4SPACES + CMT_CONTENT_IMPLIES_METHOD1 + NL); + String leftText = leftExpression.getExpressionText(); + methodsCommentList_Adding.append(_4SPACES + String.format(CMT_CONTENT_IMPLIES_METHOD2, leftText) + NL); + methodsCommentList_Adding.append(_4SPACES + CMT_CONTENT_IMPLIES_METHOD3 + constraint.getName() + NL); + methodsCommentList_Adding.append(_4SPACES + CMT_CONTENT_IMPLIES_METHOD4 + constraint.getExpression().getExpressionText()); + + if (isIncludeLambdaExpression(leftExpression)) { + List<Variable> list = getVariables(leftExpression); + + for (int i = 0; i < list.size(); i++) { + Variable variable = list.get(i); + String varName = variableNameMap.get(variable); + String define = String.format(VARIABLE_DEFINE, varName); + + constraintList_Adding.append(_8SPACES + VARIABLE_CMT + variable.getName() + NL); + constraintList_Adding.append(_8SPACES + define + NL); + constraintList_Adding.append(_8SPACES + varName + ARRAY_TOP + String.format(SET_VARIABLE_VALUE, variable.getName()) + NL); + } + constraintList_Adding.append(NL); + } + + // constraint + String expression = getContextString(leftExpression); + String label = STR_QUOTE + NUMBER_ZERO + constraint.getName() + STR_QUOTE; + constraintList_Adding.append(_8SPACES + CONSTR_LIST_ADD + OPEN + EX_CTX_MK_EQ + OPEN + expression + COMMA + EX_CTX_MK_TRUE + CLOSE + CLOSE + END + NL); + constraintList_Adding.append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + label + CLOSE + CLOSE + END + NL); + + template.implies_constrName = label; + template.implies_constraints_comment_code = methodsCommentList_Adding.toString(); + template.implies_constraints_methodName_code = _4SPACES + String.format(IMPLIES_CONSTRAINT_METHOD, methodName); + template.implies_constraints_true_code = constraintList_Adding.toString(); + + return template.getImpliesConstraintMethodCode(allConstMethodName); + } + + private String getInvarianceConstraintStr(boolean isPre) { + StringBuilder invariance_constr_Adding = new StringBuilder(); + + invariance_constr_Adding.append(getInvarianceConstraintStr_IN01(isPre)); + invariance_constr_Adding.append(NL); + invariance_constr_Adding.append(getInvarianceConstraintStr_IN02(isPre)); + invariance_constr_Adding.append(NL); + invariance_constr_Adding.append(getInvarianceConstraintStr_IN03(isPre)); + + return invariance_constr_Adding.toString(); + } + + private String getInvarianceConstraintStr_IN01(boolean isPre) { + String preLabel = ""; + String opDisplayingContent = OP_DISPLAYING_CONTENT; + if (isPre) { + opDisplayingContent = OP_PRE_DISPLAYING_CONTENT; + preLabel = "(pre)"; + } + return getInvarianceConstraintStr_IN01_IN03_Impl(preLabel, opDisplayingContent, "IN01"); + } + + private String getInvarianceConstraintStr_IN01_IN03_Impl(String preLabel, String expr, String inKind) { + StringBuilder invariance_constr_Adding = new StringBuilder(); + + invariance_constr_Adding.append(_8SPACES + "// Area." + expr + " == contentsList.get(n) OR Area." + expr + " == contentsList.get(n+1) ...)"); + invariance_constr_Adding.append(NL); + + for (int i = 0; i < allocatableList.size(); i++) { + Allocatable mainArea = allocatableList.get(i); + String leftLabel = mainArea.getName() + "." + expr + " == "; + String areaMkInt = EX_CTX_MK_INT + OPEN + String.valueOf(i + 1) + CLOSE; + String leftconstr = EX_CTX_MK_EQ + OPEN + EX_CTX_MK_SELECT + OPEN + expr + COMMA + areaMkInt + CLOSE + COMMA; + + StringBuffer constrLabel = new StringBuffer(); + StringBuffer constr = new StringBuffer(); + + constrLabel.append(STR_QUOTE + inKind +":Constraint " + preLabel + "_" + String.valueOf(i + 1) + " - (" + leftLabel); + + List<Content> mainContents = mainArea.getContentsList(); + + int childSize = mainContents.size(); + if (childSize == 0) { + constrLabel.append("NULL"); + constr.append(leftconstr + "defNull" + CLOSE); + } else { + for (int k = 0; k < mainContents.size(); k++) { + Content content = mainContents.get(k); + String contentName = content.getName(); + + int index = contentList.indexOf(content); + String contentMkInt = EX_CTX_MK_INT + OPEN + String.valueOf(index + 1) + CLOSE; + String subConstr = ""; + if (k == 0 && k != mainContents.size() - 1) { + subConstr = EX_CTX_MK_OR + OPEN; + } + + constrLabel.append(contentName); + constr.append(subConstr + leftconstr + contentMkInt + CLOSE); + + if (k != mainContents.size() - 1) { + constrLabel.append(" OR "); + constr.append(COMMA); + } else { + if (mainContents.size() != 1) { + constr.append(CLOSE); + } + } + } + } + constrLabel.append(")" + STR_QUOTE); + + invariance_constr_Adding.append(_8SPACES + CONSTR_LIST_ADD + OPEN + constr.toString() + CLOSE + END + NL); + invariance_constr_Adding.append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + constrLabel.toString() + CLOSE + CLOSE + END + NL); + } + + return invariance_constr_Adding.toString(); + } + + private String getInvarianceConstraintStr_IN02(boolean isPre) { + + int constNum = 1; + StringBuilder invariance_constr_Adding = new StringBuilder(); + String opIsDisplayed = OP_IS_DISPLAYED; + String opIsVisible = OP_IS_VISIBLE; + String preLabel = ""; + if (isPre) { + opIsDisplayed = OP_PRE_IS_DISPLAYED; + opIsVisible = OP_PRE_IS_VISIBLE; + preLabel = "(pre)"; + } + + invariance_constr_Adding.append(_8SPACES + "// a." + opIsDisplayed + "->c." + opIsVisible + " AND c." + opIsVisible + "->a." + opIsDisplayed); + invariance_constr_Adding.append(NL); + + for (int i = 0; i < allocatableList.size(); i++) { + Allocatable mainArea = allocatableList.get(i); + String areaIsDisplayed = mainArea.getName() + "." + opIsDisplayed; + String areaMkInt = EX_CTX_MK_INT + OPEN + String.valueOf(i + 1) + CLOSE; + + List<Content> mainContents = mainArea.getContentsList(); + + if (mainContents.size() != 1) { + continue; + } + + for (int j = 0; j < mainContents.size(); j++) { + StringBuffer constrLabel = new StringBuffer(); + StringBuffer constr = new StringBuffer(); + Content mainContent = mainContents.get(j); + + if (mainContent.getAllocatableList().size() != 1) { + continue; + } + + int index = contentList.indexOf(mainContent); + String contentIsVisible = mainContent.getName() + "." + opIsVisible; + String mainContentMkInt = EX_CTX_MK_INT + OPEN + String.valueOf(index + 1) + CLOSE; + + constrLabel.append(STR_QUOTE + "IN02:Constraint" + preLabel + "_" + String.valueOf(constNum) + " - " + areaIsDisplayed + " -> " + contentIsVisible + " AND " + + contentIsVisible + " -> " + areaIsDisplayed + STR_QUOTE); + constNum++; + + constr.append(EX_CTX_MK_AND + OPEN); + constr.append(EX_CTX_MK_IMPLIES + OPEN + EX_BOOL_EXPR + EX_CTX_MK_SELECT + OPEN + opIsDisplayed + COMMA + areaMkInt + CLOSE + COMMA + EX_BOOL_EXPR + + EX_CTX_MK_SELECT + OPEN + opIsVisible + COMMA + mainContentMkInt + CLOSE + CLOSE); + constr.append(COMMA); + constr.append(EX_CTX_MK_IMPLIES + OPEN + EX_BOOL_EXPR + EX_CTX_MK_SELECT + OPEN + opIsVisible + COMMA + mainContentMkInt + CLOSE + COMMA + EX_BOOL_EXPR + + EX_CTX_MK_SELECT + OPEN + opIsDisplayed + COMMA + areaMkInt + CLOSE + CLOSE); + constr.append(CLOSE); + + invariance_constr_Adding.append(_8SPACES + CONSTR_LIST_ADD + OPEN + constr.toString() + CLOSE + END + NL); + invariance_constr_Adding.append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + constrLabel.toString() + CLOSE + CLOSE + END + NL); + } + } + + return invariance_constr_Adding.toString(); + } + + private String getInvarianceConstraintStr_IN03(boolean isPre) { + String preLabel = ""; + String opAllocatedContent = OP_ALLOCATED_CONTENT; + if (isPre) { + opAllocatedContent = OP_PRE_ALLOCATED_CONTENT; + preLabel = "(pre)"; + } + return getInvarianceConstraintStr_IN01_IN03_Impl(preLabel, opAllocatedContent, "IN03"); + } + + private boolean isIncludeLambdaExpression(Expression expression) { + + for (Iterator<EObject> iterator = expression.eAllContents(); iterator.hasNext();) { + EObject object = iterator.next(); + if (object instanceof LambdaContext | object instanceof LambdaExpression) { + return true; + } + } + return false; + } + + private List<Variable> getVariables(Expression expression) { + List<Variable> list = new ArrayList<Variable>(); + + for (Iterator<EObject> iterator = expression.eAllContents(); iterator.hasNext();) { + EObject object = iterator.next(); + if (object instanceof Variable) { + list.add((Variable) object); + } + } + return list; + } + + private boolean isImplieseOperator(Expression expression) { + if (expression instanceof ImpliesOperator) { + return true; + } + return false; + } + + private boolean isBoolOperator(Expression expression) { + if (expression instanceof IsVisible) { + return true; + } else if (expression instanceof IsDisplayed) { + return true; + } else if (expression instanceof IsActive) { + return true; + } else if (expression instanceof IsHidden) { + return true; + } else if (expression instanceof IfStatement) { + return true; + } else if (expression instanceof IsDisappeared) { + return true; + } else if (expression instanceof IsCanceled) { + return true; + } else if (expression instanceof IsMuted) { + return true; + } else if (expression instanceof IsOutputted) { + return true; + } else if (expression instanceof IsAttenuated) { + return true; + } else if (expression instanceof IsSounding) { + return true; + } else if (expression instanceof IsOn) { + return true; + } else if (expression instanceof HasBeenDisplayed) { + return true; + } else if (expression instanceof HasComeEarlierThan) { + return true; + } else if (expression instanceof HasComeLaterThan) { + return true; + } + return false; + } + + private String getStoreExpr(Allocatable allocatable) { + String context = EMP_ARRAY_CONST; + + List<Content> contentsList = allocatable.getContentsList(); + + for (int i = 0; i < contentList.size(); i++) { + Content content = contentList.get(i); + if (contentsList.contains(content)) { + context = String.format(STORE_TEMPLATE, context, (i + 1)); + } + } + + return context; + } + + private String getStoreExpr(Content content) { + String context = EMP_ARRAY_CONST; + + for (int i = 0; i < allocatableList.size(); i++) { + Allocatable area = allocatableList.get(i); + if (content.getAllocatableList().contains(area)) { + context = String.format(STORE_TEMPLATE, context, (i + 1)); + } + } + + return context; + } + + private String getStoreExpr(AllocatableSet allocatableSet) { + String context = EMP_ARRAY_CONST; + List<RuleObject> set = getRuleObjectsBySet(allocatableSet, new ArrayList<RuleObject>()); + + for (int i = 0; i < allocatableList.size(); i++) { + Allocatable area = allocatableList.get(i); + if (set.contains(area)) { + context = String.format(STORE_TEMPLATE, context, (i + 1)); + } + } + + return context; + } + + private String getStoreExpr(ContentSet contentSet) { + String context = EMP_ARRAY_CONST; + List<RuleObject> set = getRuleObjectsBySet(contentSet, new ArrayList<RuleObject>()); + + for (int i = 0; i < contentList.size(); i++) { + Content content = contentList.get(i); + if (set.contains(content)) { + context = String.format(STORE_TEMPLATE, context, (i + 1)); + } + } + + return context; + } + + private String getStoreExpr(SetOfOperator op) { + String context = EMP_ARRAY_CONST; + + List<RuleObject> objects = new ArrayList<RuleObject>(); + EList<Expression> operand = op.getOperand(); + if (operand.isEmpty()) { + return context; + } + + for (Expression expression : operand) { + if (!(expression instanceof ObjectReference)) { + continue; + } + + RuleObject refObject = ((ObjectReference) expression).getRefObject(); + if (refObject instanceof Content || refObject instanceof Allocatable) { + objects.add(refObject); + } else if (refObject instanceof ContentSet | refObject instanceof AllocatableSet) { + objects.addAll(getRuleObjectsBySet(refObject, new ArrayList<RuleObject>())); + } + } + + if (objects.isEmpty()) { + return context; + } + + if (objects.get(0) instanceof Area) { + for (int i = 0; i < allocatableList.size(); i++) { + Allocatable area = allocatableList.get(i); + if (objects.contains(area)) { + context = String.format(STORE_TEMPLATE, context, (i + 1)); + } + } + } else if (objects.get(0) instanceof Zone) { + for (int i = 0; i < allocatableList.size(); i++) { + Allocatable zone = allocatableList.get(i); + if (objects.contains(zone)) { + context = String.format(STORE_TEMPLATE, context, (i + 1)); + } + } + } else if (objects.get(0) instanceof ViewContent) { + for (int i = 0; i < contentList.size(); i++) { + Content content = contentList.get(i); + if (objects.contains(content)) { + context = String.format(STORE_TEMPLATE, context, (i + 1)); + } + } + } else if (objects.get(0) instanceof SoundContent) { + for (int i = 0; i < contentList.size(); i++) { + Content content = contentList.get(i); + if (objects.contains(content)) { + context = String.format(STORE_TEMPLATE, context, (i + 1)); + } + } + } + + return context; + } + + private List<RuleObject> getRuleObjectsBySet(RuleObject refObject, List<RuleObject> elementSetList) { + Set<RuleObject> sets = new HashSet<RuleObject>(); + + if (refObject instanceof AllocatableSet) { + AllocatableSet set = (AllocatableSet) refObject; + for (AbstractAllocatable abst : set.getTarget()) { + if (abst instanceof Allocatable) { + sets.add(abst); + } else if (abst instanceof AllocatableSet) { + if (!elementSetList.contains(abst)) { + elementSetList.add(abst); + sets.addAll(getRuleObjectsBySet(abst, elementSetList)); + } + } + } + } + if (refObject instanceof ContentSet) { + ContentSet set = (ContentSet) refObject; + for (AbstractContent abst : set.getTarget()) { + if (abst instanceof Content) { + sets.add(abst); + } else if (abst instanceof ContentSet) { + if (!elementSetList.contains(abst)) { + elementSetList.add(abst); + sets.addAll(getRuleObjectsBySet(abst, elementSetList)); + } + } + } + } + + return new ArrayList<RuleObject>(sets); + } + + private String getContents(Allocatable allocatable) { + String contentStr = ""; + List<Content> contents = allocatable.getContentsList(); + + for (Content content : contents) { + contentStr += content.getName(); + if (contents.indexOf(content) != contents.size() - 1) { + contentStr += COMMA + " "; + } + } + return contentStr; + } + + private String getAllocatables(Content content) { + String areas = ""; + EList<Allocatable> allocatables = content.getAllocatableList(); + for (AbstractAllocatable allocatable : allocatables) { + areas += allocatable.getName(); + if (allocatables.indexOf(allocatable) != allocatables.size() - 1) { + areas += COMMA + " "; + } + } + return areas; + } + + private String getAreas(AllocatableSet set) { + String areas = ""; + + for (AbstractAllocatable area : set.getTarget()) { + areas += area.getName(); + if (set.getTarget().indexOf(area) != set.getTarget().size() - 1) { + areas += COMMA + " "; + } + } + return areas; + } + + private String getContents(ContentSet contentSet) { + String contents = ""; + + for (AbstractContent content : contentSet.getTarget()) { + contents += content.getName(); + if (contentSet.getTarget().indexOf(content) != contentSet.getTarget().size() - 1) { + contents += COMMA + " "; + } + } + return contents; + } + + private String getContextString(Expression expression) { + String contextString = null; + + if (expression instanceof ComplexExpression) { + contextString = getContextString(((ComplexExpression) expression).getOtherExpression()); + } else if (expression instanceof AndOperator) { + contextString = resolveExpression((AndOperator) expression); + } else if (expression instanceof OrOperator) { + contextString = resolveExpression((OrOperator) expression); + } else if (expression instanceof NotOperator) { + contextString = resolveExpression((NotOperator) expression); + } else if (expression instanceof ImpliesOperator) { + contextString = resolveExpression((ImpliesOperator) expression); + } else if (expression instanceof ObjectCompare) { + contextString = resolveExpression((ObjectCompare) expression); + } else if (expression instanceof IsEqualToOperator) { + contextString = resolveExpression((IsEqualToOperator) expression); + } else if (expression instanceof IsGreaterThanOperator) { + contextString = resolveExpression((IsGreaterThanOperator) expression); + } else if (expression instanceof IsGreaterThanEqualOperator) { + contextString = resolveExpression((IsGreaterThanEqualOperator) expression); + } else if (expression instanceof IsLowerThanOperator) { + contextString = resolveExpression((IsLowerThanOperator) expression); + } else if (expression instanceof IsLowerThanEqualOperator) { + contextString = resolveExpression((IsLowerThanEqualOperator) expression); + } else if (expression instanceof IsDisplayed) { + contextString = resolveExpression((IsDisplayed) expression); + } else if (expression instanceof DisplayingContent) { + contextString = resolveExpression((DisplayingContent) expression); + } else if (expression instanceof AllocatedContent) { + contextString = resolveExpression((AllocatedContent) expression); + } else if (expression instanceof GetContentsList) { + System.out.println("GetContentsList is not supported yet!"); + } else if (expression instanceof IsHidden) { + contextString = resolveExpression((IsHidden) expression); + } else if (expression instanceof IsActive) { + contextString = resolveExpression((IsActive) expression); + } else if (expression instanceof IsVisible) { + contextString = resolveExpression((IsVisible) expression); + } else if (expression instanceof GetAllocatables) { + System.out.println("GetAllocatables is not supported yet!"); + } else if (expression instanceof ContentValue) { + contextString = resolveExpression((ContentValue) expression); + } else if (expression instanceof ExistsOperator) { + contextString = resolveExpression((ExistsOperator) expression); + } else if (expression instanceof ForAllOperator) { + contextString = resolveExpression((ForAllOperator) expression); + } else if (expression instanceof IfStatement) { + contextString = resolveExpression((IfStatement) expression); + } else if (expression instanceof IsOn) { + contextString = resolveExpression((IsOn) expression); + } else if (expression instanceof ObjectReference) { + contextString = resolveExpression((ObjectReference) expression); + } else if (expression instanceof PreviousModifier) { + contextString = resolveExpression((PreviousModifier) expression); + } else if (expression instanceof IsDisappeared) { + contextString = resolveExpression((IsDisappeared) expression); + } else if (expression instanceof IsCanceled) { + contextString = resolveExpression((IsCanceled) expression); + } else if (expression instanceof IsMuted) { + contextString = resolveExpression((IsMuted) expression); + } else if (expression instanceof IsSounding) { + contextString = resolveExpression((IsSounding) expression); + } else if (expression instanceof OutputtingSound) { + contextString = resolveExpression((OutputtingSound) expression); + } else if (expression instanceof IsAttenuated) { + contextString = resolveExpression((IsAttenuated) expression); + } else if (expression instanceof IsOutputted) { + contextString = resolveExpression((IsOutputted) expression); + } else if (expression instanceof GetProperty) { + contextString = resolveExpression((GetProperty) expression); + } else if (expression instanceof IntegerValue) { + contextString = resolveExpression((IntegerValue) expression); + } else if (expression instanceof HasComeEarlierThan) { + contextString = resolveExpression((HasComeEarlierThan) expression); + } else if (expression instanceof HasComeLaterThan) { + contextString = resolveExpression((HasComeLaterThan) expression); + } else if (expression instanceof HasBeenDisplayed) { + contextString = resolveExpression((HasBeenDisplayed) expression); + } else if (expression instanceof SugarExpression) { + contextString = getContextString(((SugarExpression) expression).getExpanded()); + } else { + // TODO Specification not found + throw new RuntimeException("Expected Expression type is not supported yet! : " + expression.getExpressionText()); + } + + return contextString; + } + + private String resolveExpression(AndOperator expression) { + List<Expression> operand = expression.getOperand(); + String context = EX_CTX_MK_AND + OPEN; + for (int i = 0; i < operand.size(); i++) { + Expression op = operand.get(i); + String opContext = getContextString(op); + context += EX_BOOL_EXPR + opContext; + + if (i != operand.size() - 1) { + context += COMMA; + } + } + + return context + CLOSE; + } + + private String resolveExpression(OrOperator expression) { + List<Expression> operand = expression.getOperand(); + + String context = EX_CTX_MK_OR + OPEN; + for (int i = 0; i < operand.size(); i++) { + Expression op = operand.get(i); + String opContext = getContextString(op); + context += EX_BOOL_EXPR + opContext; + + if (i != operand.size() - 1) { + context += COMMA; + } + } + + return context + CLOSE; + } + + private String resolveExpression(NotOperator expression) { + List<Expression> operand = ((NotOperator) expression).getOperand(); + String context = getContextString(operand.get(0)); + + return EX_CTX_MK_NOT + OPEN + EX_BOOL_EXPR + context + CLOSE; + } + + private String resolveExpression(ImpliesOperator expression) { + List<Expression> operand = ((ImpliesOperator) expression).getOperand(); + String leftContext = getContextString(operand.get(0)); + String rightContext = getContextString(operand.get(1)); + + return EX_CTX_MK_IMPLIES + OPEN + EX_BOOL_EXPR + leftContext + COMMA + EX_BOOL_EXPR + rightContext + CLOSE; + } + + private String resolveExpression(ObjectCompare expression) { + List<Expression> operand = expression.getOperand(); + String leftCast = EX_BOOL_EXPR; + String rightCast = EX_BOOL_EXPR; + if ((operand.get(0) instanceof ContentValue) || (operand.get(0) instanceof DisplayingContent) || (operand.get(0) instanceof AllocatedContent) + || (operand.get(0) instanceof OutputtingSound) || (operand.get(0) instanceof GetProperty) || (operand.get(0) instanceof ObjectReference)) { + leftCast = EX_INT_EXPR; + } + if ((operand.get(1) instanceof ContentValue) || (operand.get(1) instanceof DisplayingContent) || (operand.get(1) instanceof AllocatedContent) + || (operand.get(1) instanceof OutputtingSound) || (operand.get(1) instanceof GetProperty) || (operand.get(1) instanceof ObjectReference)) { + rightCast = EX_INT_EXPR; + } + + String leftContext = getContextString(operand.get(0)); + String rightContext = getContextString(operand.get(1)); + + return EX_CTX_MK_EQ + OPEN + leftCast + leftContext + COMMA + rightCast + rightContext + CLOSE; + } + + private String resolveExpression(IsLowerThanEqualOperator expression) { + List<Expression> operand = expression.getOperand(); + String leftContext = getContextString(operand.get(0)); + String rightContext = getContextString(operand.get(1)); + + return EX_CTX_MK_LE + OPEN + EX_INT_EXPR + leftContext + COMMA + EX_INT_EXPR + rightContext + CLOSE; + } + + private String resolveExpression(IsLowerThanOperator expression) { + List<Expression> operand = expression.getOperand(); + String leftContext = getContextString(operand.get(0)); + String rightContext = getContextString(operand.get(1)); + + return EX_CTX_MK_LT + OPEN + EX_INT_EXPR + leftContext + COMMA + EX_INT_EXPR + rightContext + CLOSE; + } + + private String resolveExpression(IsGreaterThanEqualOperator expression) { + List<Expression> operand = expression.getOperand(); + String leftContext = getContextString(operand.get(0)); + String rightContext = getContextString(operand.get(1)); + + return EX_CTX_MK_GE + OPEN + EX_INT_EXPR + leftContext + COMMA + EX_INT_EXPR + rightContext + CLOSE; + } + + private String resolveExpression(IsGreaterThanOperator expression) { + List<Expression> operand = expression.getOperand(); + String leftContext = getContextString(operand.get(0)); + String rightContext = getContextString(operand.get(1)); + + return EX_CTX_MK_GT + OPEN + EX_INT_EXPR + leftContext + COMMA + EX_INT_EXPR + rightContext + CLOSE; + } + + private String resolveExpression(IsEqualToOperator expression) { + List<Expression> operand = expression.getOperand(); + String cast = EX_INT_EXPR; + + String leftContext = getContextString(operand.get(0)); + String rightContext = getContextString(operand.get(1)); + + return EX_CTX_MK_EQ + OPEN + cast + leftContext + COMMA + cast + rightContext + CLOSE; + } + + private String resolveExpression(ExistsOperator expression) { + return resolveExpression(expression, EX_CTX_MK_EXISTS, ""); + } + + private String resolveExpression(ForAllOperator expression) { + return resolveExpression(expression, EX_CTX_MK_FORALL, EX_CTX_MK_IMPLIES); + } + + private String resolveExpression(LambdaContext expression, String mkMethod, String implies) { + LambdaExpression lambda = expression.getLambda(); + Variable x = lambda.getX(); + + EList<Expression> operand = expression.getOperand(); + + String size = ""; + String setName = ""; + String variableName = variableNameMap.get(x); + if (operand.get(0) instanceof ObjectReference) { + ObjectReference ref = (ObjectReference) operand.get(0); + if (ref.getUnderlyingType() == ExpressionType.SET_OF_AREA || ref.getUnderlyingType() == ExpressionType.SET_OF_ZONE) { + size = ALLOCATABLE_SIZE; + } else if (ref.getUnderlyingType() == ExpressionType.SET_OF_CONTENT || ref.getUnderlyingType() == ExpressionType.SET_OF_SOUND) { + size = CONTENT_SIZE; + } + + setName = resolveExpression((ObjectReference) operand.get(0)); + + } else if (operand.get(0) instanceof GetAllocatables) { + size = CONTENT_SIZE; + + GetAllocatables getAllocatable = (GetAllocatables) operand.get(0); + if (getAllocatable.getOperand().get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) getAllocatable.getOperand().get(0); + String select = resolveExpression(pre.getObjReference()); + setName = EX_ARRAY_EXPR_CATS + EX_CTX_MK_SELECT + OPEN + OP_PRE_ALLOCATABLE + COMMA + select + CLOSE; + } else { + String select = resolveExpression((ObjectReference) getAllocatable.getOperand().get(0)); + setName = EX_ARRAY_EXPR_CATS + EX_CTX_MK_SELECT + OPEN + OP_ALLOCATABLE + COMMA + select + CLOSE; + } + + } else if (operand.get(0) instanceof GetContentsList) { + size = ALLOCATABLE_SIZE; + + GetContentsList getContentsList = (GetContentsList) operand.get(0); + if (getContentsList.getOperand().get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) getContentsList.getOperand().get(0); + String select = resolveExpression(pre.getObjReference()); + setName = EX_ARRAY_EXPR_CATS + EX_CTX_MK_SELECT + OPEN + OP_PRE_CONTENTS_LIST + COMMA + select + CLOSE; + } else { + String select = resolveExpression((ObjectReference) getContentsList.getOperand().get(0)); + setName = EX_ARRAY_EXPR_CATS + EX_CTX_MK_SELECT + OPEN + OP_CONTENTS_LIST + COMMA + select + CLOSE; + } + + } else if (operand.get(0) instanceof AllInstanceOfArea) { + size = ALLOCATABLE_SIZE; + setName = ALL_AREA_CONST; + } else if (operand.get(0) instanceof AllInstanceOfZone) { + size = ALLOCATABLE_SIZE; + setName = ALL_ZONE_CONST; + } else if (operand.get(0) instanceof AllInstanceOfViewContent) { + size = CONTENT_SIZE; + setName = ALL_VIEWCONTENT_CONST; + } else if (operand.get(0) instanceof AllInstanceOfSoundContent) { + size = CONTENT_SIZE; + setName = ALL_SOUNDCONTENT_CONST; + } else if (operand.get(0) instanceof SetOfOperator) { + SetOfOperator setOfOp = (SetOfOperator) operand.get(0); + if (setOfOp.getUnderlyingType() == ExpressionType.SET_OF_AREA || setOfOp.getUnderlyingType() == ExpressionType.SET_OF_ZONE) { + size = ALLOCATABLE_SIZE; + } else if (setOfOp.getUnderlyingType() == ExpressionType.SET_OF_CONTENT || setOfOp.getUnderlyingType() == ExpressionType.SET_OF_SOUND) { + size = CONTENT_SIZE; + } + + String expressionText = setOfOp.getExpressionText(); + setName = SetOfNameMap.get(expressionText); + } else if (operand.get(0) instanceof ActiveContents) { + size = CONTENT_SIZE; + ActiveContents activeContents = (ActiveContents) operand.get(0); + if (activeContents.getOperand().get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) activeContents.getOperand().get(0); + String select = resolveExpression(pre.getObjReference()); + setName = EX_ARRAY_EXPR_CATS + EX_CTX_MK_SELECT + OPEN + OP_PRE_ACTIVE_CONTENTS + COMMA + select + CLOSE; + } else { + String select = resolveExpression((ObjectReference) activeContents.getOperand().get(0)); + setName = EX_ARRAY_EXPR_CATS + EX_CTX_MK_SELECT + OPEN + OP_ACTIVE_CONTENTS + COMMA + select + CLOSE; + } + } + + String setContext = EX_CTX_MK_SELECT + OPEN + setName + COMMA + variableName + ARRAY_TOP + CLOSE; + String expContext = getContextString(lambda.getBodyText()); + String rangeContext = EX_CTX_MK_AND + OPEN + EX_CTX_MK_LE + OPEN + EX_CTX_MK_INT + OPEN + 1 + CLOSE + COMMA + EX_ARITH_EXPR + variableName + ARRAY_TOP + CLOSE + COMMA + + EX_CTX_MK_LE + OPEN + EX_ARITH_EXPR + variableName + ARRAY_TOP + COMMA + size + CLOSE + CLOSE; + String bodyContext = EX_CTX_MK_AND + OPEN + rangeContext + COMMA + EX_BOOL_EXPR + setContext; + + if (!implies.isEmpty()) { + bodyContext = implies + OPEN + bodyContext + CLOSE + COMMA + EX_BOOL_EXPR + expContext + CLOSE; + } else { + bodyContext += COMMA + EX_BOOL_EXPR + expContext + CLOSE; + } + + String context = mkMethod + OPEN + variableName + COMMA + bodyContext + COMMA + 1 + COMMA + NULL_STRING + COMMA + NULL_STRING + COMMA + NULL_STRING + COMMA + NULL_STRING + + CLOSE; + return context; + } + + private String resolveExpression(IsDisplayed expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_DISPLAYED + COMMA + context + CLOSE; + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_DISPLAYED + COMMA + context + CLOSE; + } + + private String resolveExpression(IsVisible expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_VISIBLE + COMMA + context + CLOSE; + } + + String context = getContextString(operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_VISIBLE + COMMA + context + CLOSE; + } + + private String resolveExpression(IsHidden expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_HIDDEN + COMMA + context + CLOSE; + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_HIDDEN + COMMA + context + CLOSE; + } + + private String resolveExpression(IsActive expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_ACTIVE + COMMA + context + CLOSE; + } + + String context = getContextString(operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_ACTIVE + COMMA + context + CLOSE; + } + + private String resolveExpression(DisplayingContent expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_DISPLAYING_CONTENT + COMMA + context + CLOSE; + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_DISPLAYING_CONTENT + COMMA + context + CLOSE; + } + + private String resolveExpression(AllocatedContent expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_ALLOCATED_CONTENT + COMMA + context + CLOSE; + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_ALLOCATED_CONTENT + COMMA + context + CLOSE; + } + + private String resolveExpression(ContentValue expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_CONTENT_VALUE + COMMA + context + CLOSE; + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_CONTENT_VALUE + COMMA + context + CLOSE; + } + + private String resolveExpression(IsMuted expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_MUTED + COMMA + context + CLOSE; + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_MUTED + COMMA + context + CLOSE; + } + + private String resolveExpression(IsOutputted expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_OUTPUTTED + COMMA + context + CLOSE; + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_OUTPUTTED + COMMA + context + CLOSE; + } + + private String resolveExpression(IsAttenuated expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_ATTENUATED + COMMA + context + CLOSE; + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_ATTENUATED + COMMA + context + CLOSE; + } + + private String resolveExpression(OutputtingSound expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_OUTPUTTING_SOUND + COMMA + context + CLOSE; + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_OUTPUTTING_SOUND + COMMA + context + CLOSE; + } + + private String resolveExpression(IsSounding expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_SOUNDING + COMMA + context + CLOSE; + } + + String context = getContextString(operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_SOUNDING + COMMA + context + CLOSE; + } + + private String resolveExpression(GetProperty expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return String.format(context, OP_PRE_GET_PROPERTY); + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return String.format(context, OP_GET_PROPERTY); + } + + private String resolveExpression(IntegerValue expression) { + int value = expression.getValue(); + return EX_CTX_MK_INT + OPEN + String.valueOf(value) + CLOSE; + } + + private String resolveExpression(IfStatement expression) { + + Expression condition = expression.getCondition(); + Expression thenExpression = expression.getThenExpression(); + Expression elseExpression = expression.getElseExpression(); + + String conditionContext = getContextString(condition); + String thenContext = getContextString(thenExpression); + String elseContext = getContextString(elseExpression); + + String context = EX_CTX_MK_ITE + OPEN + EX_BOOL_EXPR + conditionContext + COMMA + thenContext + COMMA + elseContext + CLOSE; + return context; + } + + private String resolveExpression(IsOn expression) { + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + String context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_ON + COMMA + context + CLOSE; + } else if (!(operand.get(0) instanceof ObjectReference)) { + String context = getContextString(operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_ON + COMMA + context + CLOSE; + } + + String context = resolveExpression((ObjectReference) operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_ON + COMMA + context + CLOSE; + } + + private String resolveExpression(ObjectReference expression) { + if (expression.getRefObject() instanceof Area) { + Area target = (Area) expression.getRefObject(); + for (int i = 0; i < allocatableList.size(); i++) { + Allocatable area = allocatableList.get(i); + if (target == area) { + return EX_CTX_MK_INT + OPEN + (i + 1) + CLOSE; + } + } + } else if (expression.getRefObject() instanceof Zone) { + Zone target = (Zone) expression.getRefObject(); + for (int i = 0; i < allocatableList.size(); i++) { + Allocatable allocatable = allocatableList.get(i); + if (target == allocatable) { + return EX_CTX_MK_INT + OPEN + (i + 1) + CLOSE; + } + } + } else if (expression.getRefObject() instanceof ViewContent) { + Content target = (Content) expression.getRefObject(); + for (int i = 0; i < contentList.size(); i++) { + Content content = contentList.get(i); + if (target == content) { + return EX_CTX_MK_INT + OPEN + (i + 1) + CLOSE; + } + } + } else if (expression.getRefObject() instanceof SoundContent) { + Content target = (Content) expression.getRefObject(); + for (int i = 0; i < contentList.size(); i++) { + Content content = contentList.get(i); + if (target == content) { + return EX_CTX_MK_INT + OPEN + (i + 1) + CLOSE; + } + } + } else if (expression.getRefObject() instanceof Variable) { + Variable target = (Variable) expression.getRefObject(); + + if ((expression.eContainer() instanceof GetAllocatables) || (expression.eContainer() instanceof GetContentsList)) { + return EX_CTX_MK_INT_CONST + OPEN + EX_CTX_MK_SYMBOL + OPEN + STR_QUOTE + target.getName() + STR_QUOTE + CLOSE + CLOSE; + } + + return variableNameMap.get(target) + ARRAY_TOP; + } else if (expression.getRefObject() instanceof AllocatableSet) { + AllocatableSet target = (AllocatableSet) expression.getRefObject(); + return allocatableSetNameMap.get(target); + } else if (expression.getRefObject() instanceof ContentSet) { + ContentSet target = (ContentSet) expression.getRefObject(); + return contentSetNameMap.get(target); + } else if (expression.getRefObject() instanceof Scene) { + Scene target = (Scene) expression.getRefObject(); + for (int i = 0; i < sceneList.size(); i++) { + Scene scene = sceneList.get(i); + if (target == scene) { + return EX_CTX_MK_INT + OPEN + (i + 1) + CLOSE; + } + } + } else if (expression.getRefObject() instanceof IntegerProperty) { + IntegerProperty target = (IntegerProperty) expression.getRefObject(); + Scene parent = (Scene) target.eContainer(); + + for (int i = 0; i < sceneList.size(); i++) { + Scene scene = sceneList.get(i); + if (parent == scene) { + int propIndex = scene.getProperties().indexOf(target) + 1; + + String propContext = EX_CTX_MK_SELECT + OPEN + "%s" + COMMA + EX_CTX_MK_INT + OPEN + propIndex + CLOSE + CLOSE; + return EX_CTX_MK_SELECT + OPEN + EX_ARRAY_EXPR_CATS + propContext + COMMA + EX_CTX_MK_INT + OPEN + (i + 1) + CLOSE + CLOSE; + } + } + } + return null; + } + + private String resolveExpression(PreviousModifier expression) { + String context = resolveExpression(expression.getObjReference()); + return context; + } + + private String resolveExpression(IsDisappeared expression) { + EList<Expression> operand = expression.getOperand(); + + String context = ""; + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_DISAPPEARED + COMMA + context + CLOSE; + } + + context = getContextString(operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_DISAPPEARED + COMMA + context + CLOSE; + } + + private String resolveExpression(IsCanceled expression) { + EList<Expression> operand = expression.getOperand(); + + String context = ""; + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_IS_CANCELED + COMMA + context + CLOSE; + } + + context = getContextString(operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_IS_CANCELED + COMMA + context + CLOSE; + } + + private String resolveExpression(HasBeenDisplayed expression) { + EList<Expression> operand = expression.getOperand(); + + String context = ""; + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + context = resolveExpression(pre.getObjReference()); + return EX_CTX_MK_SELECT + OPEN + OP_PRE_HAS_BEEN_DISPLAYED + COMMA + context + CLOSE; + } + + context = getContextString(operand.get(0)); + return EX_CTX_MK_SELECT + OPEN + OP_HAS_BEEN_DISPLAYED + COMMA + context + CLOSE; + } + private String resolveExpression(HasComeEarlierThan expression) { + String context = ""; + String leftContext = ""; + String rightContext = ""; + + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + leftContext = resolveExpression(pre.getObjReference()); + } else { + leftContext = getContextString(operand.get(0)); + } + + if (operand.get(1) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(1); + rightContext = resolveExpression(pre.getObjReference()); + } else { + rightContext = getContextString(operand.get(1)); + } + + String context1 = EX_ARRAY_EXPR_CATS + EX_CTX_MK_SELECT + OPEN + OP_HAS_COME_EARLIER_THAN + COMMA + leftContext + CLOSE; + context = EX_CTX_MK_SELECT + OPEN + context1 + COMMA + rightContext + CLOSE; + + return context; + } + + private String resolveExpression(HasComeLaterThan expression) { + String context = ""; + String leftContext = ""; + String rightContext = ""; + + EList<Expression> operand = expression.getOperand(); + + if (operand.get(0) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(0); + leftContext = resolveExpression(pre.getObjReference()); + } else { + leftContext = getContextString(operand.get(0)); + } + + if (operand.get(1) instanceof PreviousModifier) { + PreviousModifier pre = (PreviousModifier) operand.get(1); + rightContext = resolveExpression(pre.getObjReference()); + } else { + rightContext = getContextString(operand.get(1)); + } + + String context1 = EX_ARRAY_EXPR_CATS + EX_CTX_MK_SELECT + OPEN + OP_HAS_COME_LATER_THAN + COMMA + leftContext + CLOSE; + context = EX_CTX_MK_SELECT + OPEN + context1 + COMMA + rightContext + CLOSE; + + return context; + } + + class ImpliseConstraintInfo { + int index; + + AbstractConstraint constraint; + + String methodName; + + public int getIndex() { + return index; + } + + public String getMethodName() { + return methodName; + } + + public boolean isRuntime() { + if (constraint instanceof Constraint) { + return ((Constraint) constraint).isRuntime(); + } + return true; + } + + public void setMethodName(String methodName) { + this.methodName = methodName; + } + + public void setIndex(int index) { + this.index = index; + } + + public AbstractConstraint getConstraint() { + return constraint; + } + + public void setConstraint(AbstractConstraint constraint) { + this.constraint = constraint; + } + } +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintCodeTemplate.java b/rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintCodeTemplate.java new file mode 100644 index 0000000..1f96853 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintCodeTemplate.java @@ -0,0 +1,315 @@ +package rba.tool.editor.generator.z3; + +public class ConstraintCodeTemplate { + + String allocatable_content_set_code; + String allocatable_content_size_code; + String init_code; + String setup_code; + String constraints_code; + String implies_constraints_call_code; + String implies_constraints_method_code; + String implies_constraints_comment_code; + String implies_constraints_methodName_code; + String implies_constraints_true_code; + String implies_constrName; + String invariance_constr_code; + String invariance_pre_constr_code; + + private static final String NL = "\r\n"; + + String getCompleteCode() { + return "import groovy.transform.CompileStatic;" + NL + NL + + "import java.util.ArrayList;" + NL + + "import java.util.LinkedHashMap;" + NL + + "import java.util.List;" + NL + + "import java.util.Map;" + NL + NL + + + "import com.microsoft.z3.ArithExpr;" + NL + + "import com.microsoft.z3.ArrayExpr;" + NL + + "import com.microsoft.z3.BoolExpr;" + NL + + "import com.microsoft.z3.Context;" + NL + + "import com.microsoft.z3.Expr;" + NL + + "import com.microsoft.z3.IntExpr;" + NL + + "import com.microsoft.z3.Quantifier;" + NL + + "import com.microsoft.z3.Solver;" + NL + + "import com.microsoft.z3.Sort;" + NL + + "import com.microsoft.z3.Status;" + NL + NL + + "import com.microsoft.z3.IntNum;" + NL + NL + + + "import rba.tool.core.z3.Z3CodeManager;" + NL + NL + + + "@CompileStatic" + NL + + "public class ConstraintCalculation implements rba.tool.core.constraint.IConstraintCalculation {" + NL + NL + + " boolean onlyOnline;" + NL + + " IntNum defNull;" + NL + + " IntNum allocatableSize;" + NL + + " IntNum contentSize;" + NL + + " Context ctx;" + NL + + " Sort int_type;" + NL + + " Sort bool_type;" + NL + + " Sort array_int_bool_type;" + NL + + " Sort array_int_int_type;" + NL + + " ArrayExpr displayingContent;" + NL + + " ArrayExpr allocatedContent;" + NL + + " ArrayExpr isDisplayed;" + NL + + " ArrayExpr isHidden;" + NL + + " ArrayExpr contentsList;" + NL + + " ArrayExpr contentValue;" + NL + + " ArrayExpr isVisible;" + NL + + " ArrayExpr isActive;" + NL + + " ArrayExpr allocatable;" + NL + + " ArrayExpr preDisplayingContent;" + NL + + " ArrayExpr preAllocatedContent;" + NL + + " ArrayExpr preIsDisplayed;" + NL + + " ArrayExpr preIsHidden;" + NL + + " ArrayExpr preContentsList;" + NL + + " ArrayExpr preContentValue;" + NL + + " ArrayExpr preIsVisible;" + NL + + " ArrayExpr preIsActive;" + NL + + " ArrayExpr preAllocatable;" + NL + + " ArrayExpr isMuted;" + NL + + " ArrayExpr isOutputted;" + NL + + " ArrayExpr isAttenuated;" + NL + + " ArrayExpr outputtingSound;" + NL + + " ArrayExpr isSounding;" + NL + + " ArrayExpr preIsMuted;" + NL + + " ArrayExpr preIsOutputted;" + NL + + " ArrayExpr preIsAttenuated;" + NL + + " ArrayExpr preOutputtingSound;" + NL + + " ArrayExpr preIsSounding;" + NL + + " ArrayExpr isOn;" + NL + + " ArrayExpr getProperty;" + NL + + " ArrayExpr preIsOn;" + NL + + " ArrayExpr preGetProperty;" + NL + + " ArrayExpr isDefeatedBy;" + NL + + " ArrayExpr defeats;" + NL + + " ArrayExpr isDisappeared;" + NL + + " ArrayExpr isCanceled;" + NL + + + " ArrayExpr hasBeenDisplayed;" + NL + + " ArrayExpr hasComeEarlierThan;" + NL + + " ArrayExpr hasComeLaterThan;" + NL + + + " ArrayExpr preIsDefeatedBy;" + NL + + " ArrayExpr preDefeats;" + NL + + " ArrayExpr preIsDisappeared;" + NL + + " ArrayExpr preIsCanceled;" + NL + NL + + + " ArrayExpr activeContents;" + NL + + " ArrayExpr preActiveContents;" + NL + + " ArrayExpr preHasBeenDisplayed;" + NL + + + " ArrayExpr emp;" + NL + + " ArrayExpr empArrayConst;" + NL + + " ArrayExpr allInstanceOfArea;" + NL + + " ArrayExpr allInstanceOfAreaConst;" + NL + + " ArrayExpr allInstanceOfZone;" + NL + + " ArrayExpr allInstanceOfZoneConst;" + NL + + " ArrayExpr allInstanceOfViewContent;" + NL + + " ArrayExpr allInstanceOfViewContentConst;" + NL + NL + + " ArrayExpr allInstanceOfSoundContent;" + NL + + " ArrayExpr allInstanceOfSoundContentConst;" + NL + NL + + + allocatable_content_set_code + NL + + + " public void setUp(boolean onlyOnline) {" + NL + + " this.onlyOnline = onlyOnline;" + NL + + " ctx = new Context();" + NL + + " defNull = ctx.mkInt(0);" + NL + + allocatable_content_size_code + NL + + " int_type = ctx.getIntSort();" + NL + + " bool_type = ctx.getBoolSort();" + NL + + " array_int_bool_type = ctx.mkArraySort(int_type, bool_type);" + NL + + " array_int_int_type = ctx.mkArraySort(int_type, int_type);" + NL + NL + + + " displayingContent = ctx.mkArrayConst(\"displayingContent\", int_type, int_type);" + NL + + " allocatedContent = ctx.mkArrayConst(\"allocatedContent\", int_type, int_type);" + NL + + " isDisplayed = ctx.mkArrayConst(\"isDisplayed\", int_type, bool_type);" + NL + + " contentsList = ctx.mkArrayConst(\"contentsList\", int_type, array_int_bool_type);" + NL + + " contentValue = ctx.mkArrayConst(\"contentValue\", int_type, int_type);" + NL + + " isHidden = ctx.mkArrayConst(\"isHidden\", int_type, bool_type);" + NL + + " isVisible = ctx.mkArrayConst(\"isVisible\", int_type, bool_type);" + NL + + " isActive = ctx.mkArrayConst(\"isActive\", int_type, bool_type);" + NL + + " allocatable = ctx.mkArrayConst(\"allocatable\", int_type, array_int_bool_type);" + NL + NL + + " outputtingSound = ctx.mkArrayConst(\"outputtingSound\", int_type, int_type);" + NL + + " isOutputted = ctx.mkArrayConst(\"isOutputted\", int_type, bool_type);" + NL + + " isMuted = ctx.mkArrayConst(\"isMuted\", int_type, bool_type);" + NL + + " isAttenuated = ctx.mkArrayConst(\"isAttenuated\", int_type, bool_type);" + NL + + " isSounding = ctx.mkArrayConst(\"isSounding\", int_type, bool_type);" + NL + + + " preDisplayingContent = ctx.mkArrayConst(\"preDisplayingContent\", int_type, int_type);" + NL + + " preAllocatedContent = ctx.mkArrayConst(\"preAllocatedContent\", int_type, int_type);" + NL + + " preIsDisplayed = ctx.mkArrayConst(\"preIsDisplayed\", int_type, bool_type);" + NL + + " preContentsList = ctx.mkArrayConst(\"preContentsList\", int_type, array_int_bool_type);" + NL + + " preContentValue = ctx.mkArrayConst(\"preContentValue\", int_type, int_type);" + NL + + " preIsHidden = ctx.mkArrayConst(\"preIsHidden\", int_type, bool_type);" + NL + + " preIsVisible = ctx.mkArrayConst(\"preIsVisible\", int_type, bool_type);" + NL + + " preIsActive = ctx.mkArrayConst(\"preIsActive\", int_type, bool_type);" + NL + + " preAllocatable = ctx.mkArrayConst(\"preAllocatable\", int_type, array_int_bool_type);" + NL +NL + + " preOutputtingSound = ctx.mkArrayConst(\"preOutputtingSound\", int_type, int_type);" + NL + + " preIsOutputted = ctx.mkArrayConst(\"preIsOutputted\", int_type, bool_type);" + NL + + " preIsMuted = ctx.mkArrayConst(\"preIsMuted\", int_type, bool_type);" + NL + + " preIsAttenuated = ctx.mkArrayConst(\"preIsAttenuated\", int_type, bool_type);" + NL + + " preIsSounding = ctx.mkArrayConst(\"preIsSounding\", int_type, bool_type);" + NL + + + " isOn = ctx.mkArrayConst(\"isOn\", int_type, bool_type);" + NL + + " getProperty = ctx.mkArrayConst(\"getProperty\", int_type, array_int_int_type);" + NL + + " preIsOn = ctx.mkArrayConst(\"preIsOn\", int_type, bool_type);" + NL + + " preGetProperty = ctx.mkArrayConst(\"preGetProperty\", int_type, array_int_int_type);" + NL + + " isDefeatedBy = ctx.mkArrayConst(\"isDefeatedBy\", int_type, array_int_bool_type);" + NL + + " defeats = ctx.mkArrayConst(\"defeats\", int_type, array_int_bool_type);" + NL + + " isDisappeared = ctx.mkArrayConst(\"isDisappeared\", int_type, bool_type);" + NL + + " isCanceled = ctx.mkArrayConst(\"isCanceled\", int_type, bool_type);" + NL + + + " hasBeenDisplayed = ctx.mkArrayConst(\"hasBeenDisplayed\", int_type, bool_type);" + NL + + " hasComeEarlierThan = ctx.mkArrayConst(\"hasComeEarlierThan\", int_type, array_int_bool_type);" + NL + + " hasComeLaterThan = ctx.mkArrayConst(\"hasComeLaterThan\", int_type, array_int_bool_type);" + NL + + + " preIsDefeatedBy = ctx.mkArrayConst(\"preIsDefeatedBy\", int_type, array_int_bool_type);" + NL + + " preDefeats = ctx.mkArrayConst(\"preDefeats\", int_type, array_int_bool_type);" + NL + + " preIsDisappeared = ctx.mkArrayConst(\"preIsDisappeared\", int_type, bool_type);" + NL + + " preIsCanceled = ctx.mkArrayConst(\"preIsCanceled\", int_type, bool_type);" + NL + NL + + + " preHasBeenDisplayed = ctx.mkArrayConst(\"preHasBeenDisplayed\", int_type, bool_type);" + NL + + + " activeContents = ctx.mkArrayConst(\"activeContents\", int_type, array_int_bool_type);" + NL + + " preActiveContents = ctx.mkArrayConst(\"preActiveContents\", int_type, array_int_bool_type);" + NL + + + " emp = ctx.mkArrayConst(\"emp\", int_type, bool_type);" + NL + + " empArrayConst = ctx.mkConstArray(int_type, ctx.mkFalse());" + NL + + " allInstanceOfArea = ctx.mkArrayConst(\"allInstanceOfArea\", int_type, bool_type);" + NL + + " allInstanceOfAreaConst = ctx.mkConstArray(int_type, ctx.mkTrue());" + NL + + " allInstanceOfZone = ctx.mkArrayConst(\"allInstanceOfZone\", int_type, bool_type);" + NL + + " allInstanceOfZoneConst = ctx.mkConstArray(int_type, ctx.mkTrue());" + NL + + " allInstanceOfViewContent = ctx.mkArrayConst(\"allInstanceOfViewContent\", int_type, bool_type);" + NL + + " allInstanceOfViewContentConst = ctx.mkConstArray(int_type, ctx.mkTrue());" + NL +NL + + " allInstanceOfSoundContent = ctx.mkArrayConst(\"allInstanceOfSoundContent\", int_type, bool_type);" + NL + + " allInstanceOfSoundContentConst = ctx.mkConstArray(int_type, ctx.mkTrue());" + NL +NL + + + setup_code + NL + + " }" + NL + NL + + + " public void close() {" + NL + + " ctx.close();" + NL + + " }" + NL + NL + + + " /**" + NL + + " * Initialization of constraint list" + NL + + " */" + NL + + " private void initConstraintList(List<BoolExpr> constrList, List<BoolExpr> constrLabelList) {" + NL + + " constrList.add(ctx.mkEq(emp, empArrayConst));" + NL + + " constrLabelList.add(ctx.mkBoolConst(\"Constraint : Emp \"));" + NL + + " constrList.add(ctx.mkEq(allInstanceOfArea, allInstanceOfAreaConst));" + NL + + " constrLabelList.add(ctx.mkBoolConst(\"Constraint : AllInstanceOfArea \"));" + NL + + " constrList.add(ctx.mkEq(allInstanceOfZone, allInstanceOfZoneConst));" + NL + + " constrLabelList.add(ctx.mkBoolConst(\"Constraint : AllInstanceOfZone \"));" + NL + + " constrList.add(ctx.mkEq(allInstanceOfViewContent, allInstanceOfViewContentConst));" + NL + + " constrLabelList.add(ctx.mkBoolConst(\"Constraint : AllInstanceOfViewContent \"));" + NL + NL + + " constrList.add(ctx.mkEq(allInstanceOfSoundContent, allInstanceOfSoundContentConst));" + NL + + " constrLabelList.add(ctx.mkBoolConst(\"Constraint : AllInstanceOfSoundContent \"));" + NL + NL + + + init_code + NL + + + " }" + NL + NL + + + " /**" + NL + + " * Contradiction verification of all constraints" + NL + + " */" + NL + + " public List<String> calculateAllConstraint() {" + NL + + " Solver s = ctx.mkSolver();" + NL + + " s.push();" + NL + NL + + + " List<BoolExpr> constrList = new ArrayList<BoolExpr>();" + NL + + " List<BoolExpr> constrLabelList = new ArrayList<BoolExpr>();" + NL + NL + + + " setAllConstraintContext(constrList, constrLabelList);" + NL + NL + + + " for (int i = 0; i < constrList.size(); i++) {" + NL +// + " s.assertAndTrack(constrList.get(i), constrLabelList.get(i));" + NL + + " s.assertAndTrack((BoolExpr) constrList.get(i).simplify(), constrLabelList.get(i));" + NL + + " }" + NL + NL + + + " Status st = s.check();" + NL + + " List<String> list = Z3CodeManager.INSTNACE.getErrors(ctx, s, st,\"allConstr\" ,constrList, constrLabelList);" + NL + + " s.pop();" + NL + + " return list;" + NL + + " }" + NL + NL + + + " /**" + NL + + " * Contradiction verification execution" + NL + + " */" + NL + + " public void setAllConstraintContext(List<BoolExpr> constrList, List<BoolExpr> constrLabelList) {" + NL + + " initConstraintList(constrList, constrLabelList);" + NL + + + constraints_code + NL + + + " setInvarianceConstraintContext(constrList, constrLabelList);" + NL + + " setInvariancePreConstraintContext(constrList, constrLabelList);" + NL + + + " }" + NL + NL + + + " /**" + NL + + " * Model invariant constraints" + NL + + " */" + NL + + " public void setInvarianceConstraintContext(List<BoolExpr> constrList, List<BoolExpr> constrLabelList) {" + NL + + + invariance_constr_code + NL + + + " }" + NL + NL + + + " /**" + NL + + " * Model invariant constraint (pre constraint)" + NL + + " */" + NL + + " public void setInvariancePreConstraintContext(List<BoolExpr> constrList, List<BoolExpr> constrLabelList) {" + NL + + + invariance_pre_constr_code + NL + + + " }" + NL + NL + + + " /**" + NL + + " * Contradiction verification of implication partial constraints" + NL + + " */" + NL + + " public Map<String, List<String>> calculateImpliesConstraints() {" + NL + + " Map<String, List<String>> map = new LinkedHashMap<String, List<String>>();" + NL + + + implies_constraints_call_code + NL + + + " return map;" + NL + + " }" + NL + NL + + + implies_constraints_method_code + NL + + + "}" + NL; + + } + + String getImpliesConstraintMethodCode(String allConstMethodName) { + return " /**" + NL + + implies_constraints_comment_code + NL + + " */" + NL + + implies_constraints_methodName_code + NL + + " System.out.println(\"Calculate:\" + "+implies_constrName+");" + NL + NL + + + " Solver s = ctx.mkSolver();" + NL + + " s.push();" + NL + NL + + + " List<BoolExpr> constrList = new ArrayList<BoolExpr>();" + NL + + " List<BoolExpr> constrLabelList = new ArrayList<BoolExpr>();" + NL + NL + + + implies_constraints_true_code + NL + + + " "+allConstMethodName+"(constrList, constrLabelList);" + NL + NL + + + " for (int i = 0; i < constrList.size(); i++) {" + NL + + " s.assertAndTrack((BoolExpr) constrList.get(i).simplify(), constrLabelList.get(i));" + NL + + " }" + NL + NL + + + " Status st = s.check();" + NL + + " List<String> list = Z3CodeManager.INSTNACE.getErrors(ctx, s, st, "+implies_constrName+",constrList, constrLabelList);" + NL + + " s.pop();" + NL + + " return list;" + NL + + " }" + NL; + } + +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintGeneratorImpl.xtend b/rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintGeneratorImpl.xtend new file mode 100644 index 0000000..907f8df --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintGeneratorImpl.xtend @@ -0,0 +1,48 @@ +package rba.tool.editor.generator.z3 + +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.emf.ecore.resource.ResourceSet +import org.eclipse.xtext.generator.AbstractGenerator +import org.eclipse.xtext.generator.IFileSystemAccess2 +import org.eclipse.xtext.generator.IGeneratorContext +import rba.tool.editor.model.manager.ResourceManager + +/** + * Generates code from your model files on save. + * + * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#code-generation + */ +class ConstraintGeneratorImpl extends AbstractGenerator implements IConstraintGenerator { + + private static ConstraintCodeGenerationSupporter generationSupporter = new ConstraintCodeGenerationSupporter(); + + override doGenerate(Resource input, IFileSystemAccess2 fsa, IGeneratorContext context) { + doGenerate(input.resourceSet, fsa, context); + } + + override beforeGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + } + + override afterGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + } + + override void doGenerate(ResourceSet resourceSet, IFileSystemAccess2 fsa, IGeneratorContext context) { + fsa.generateFile("ConstraintCalculation.java", resourceSet.compile); + } + + def compile(ResourceSet resourceSet) ''' + «val allAreas = ResourceManager.INSTANCE.getRbaAreas(resourceSet)» + «val allZones = ResourceManager.INSTANCE.getRbaZones(resourceSet)» + «val allVContents = ResourceManager.INSTANCE.getRbaViewContents(resourceSet)» + «val allSContents = ResourceManager.INSTANCE.getRbaSoundContents(resourceSet)» + «val allAreaSets = ResourceManager.INSTANCE.getRbaAreaSets(resourceSet)» + «val allZoneSets = ResourceManager.INSTANCE.getRbaZoneSets(resourceSet)» + «val allVContentSets = ResourceManager.INSTANCE.getRbaViewContentSets(resourceSet)» + «val allSContentSets = ResourceManager.INSTANCE.getRbaSoundContentSets(resourceSet)» + «val allValiables = ResourceManager.INSTANCE.getRbaVariables(resourceSet)» + «val allConstraints = ResourceManager.INSTANCE.getRbaConstraints(resourceSet)» + «val allScenes = ResourceManager.INSTANCE.getRbaScenes(resourceSet)» + «val allSetOfOperators = ResourceManager.INSTANCE.getRbaSetOfOperators(resourceSet)» + «generationSupporter.generate(allVContents,allSContents, allAreas,allZones, allVContentSets,allSContentSets, allAreaSets,allZoneSets, allValiables, allConstraints, allScenes, allSetOfOperators)» + ''' +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/z3/GeneratorConstants.java b/rba.tool.editor/src/rba/tool/editor/generator/z3/GeneratorConstants.java new file mode 100644 index 0000000..7ca3b74 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/z3/GeneratorConstants.java @@ -0,0 +1,320 @@ +package rba.tool.editor.generator.z3; + +interface GeneratorConstants { + + static final String CMT_AREA_LIST = "// Area definition"; + + static final String CMT_AREA_VISIBILITY_LABEL_LIST = "// Visibility-constrained labeling"; + + static final String CMT_AREA_ZORDER_LABEL_LIST = "// Constraint expression labeling"; + + static final String CMT_CONTENT_STATE_LIST = "// Content definition"; + + static final String CMT_CONTENT_STATE_LABEL_LIST = "// Labeling Priority Constraint Expressions"; + + static final String CMT_CONTENT_STATE_PRIORITY_COMMENT_CONNECTOR = "Priority conditional expression"; + + static final String CMT_CONTENT_MULTI_START = "/**"; + + static final String CMT_CONTENT_MULTI_END = " */"; + + static final String CMT_CONTENT_IMPLIES_METHOD1 = " * Contradiction verification of implication partial constraints"; + + static final String CMT_CONTENT_IMPLIES_METHOD2 = " * %s == TRUE holds"; + + static final String CMT_CONTENT_IMPLIES_METHOD3 = " * target name : "; + + static final String CMT_CONTENT_IMPLIES_METHOD4 = " * expression text : "; + + static final String CMT_NAME_CLOSE = "]"; + + static final String CMT_NAME_OPEN = "["; + + static final String EX_NON = "non"; + + static final String EX_STD = "std"; + + static final String EX_MAX = "max"; + + static final String EX_MIN = "min"; + + static final String FUNC_ALLO_LIST = "createAlloList"; + + static final String FUNC_ALLO_VIS_CONSTR = "createAlloVisConstrList"; + + static final String FUNC_ALLO_VIS_CONSTR_LBL = "createAlloVisConstrLbl"; + + static final String FUNC_AREA_LIST = "createAreaList"; + + static final String FUNC_AREA_ZORDR_CONSTR = "createAreaZorderConstrList"; + + static final String FUNC_AREA_ZORDR_CONSTR_LBL = "createAreaZorderConstrLbl"; + + static final String FUNC_CST_LIST = "createContentList"; + + static final String FUNC_CST_CONSTR = "createConstrList"; + + static final String FUNC_CST_CONSTR_LBL = "createConstrLabelList"; + + static final String EX_CTX_MK_EQ = "ctx.mkEq"; + + static final String EX_CTX_MK_GT = "ctx.mkGt"; + + static final String EX_CTX_MK_LT = "ctx.mkLt"; + + static final String EX_CTX_MK_AND = "ctx.mkAnd"; + + static final String EX_CTX_MK_ADD = "ctx.mkAdd"; + + static final String EX_CTX_MK_INT = "ctx.mkInt"; + + static final String EX_CTX_MK_OR = "ctx.mkOr"; + + static final String EX_CTX_MK_XOR = "ctx.mkXor"; + + static final String EX_CTX_MK_NOT = "ctx.mkNot"; + + static final String EX_CTX_MK_IMPLIES = "ctx.mkImplies"; + + static final String EX_CTX_MK_GE = "ctx.mkGe"; + + static final String EX_CTX_MK_LE = "ctx.mkLe"; + + static final String EX_CTX_MK_SELECT = "ctx.mkSelect"; + + static final String EX_CTX_MK_STORE = "ctx.mkStore"; + + static final String EX_CTX_MK_EXISTS = "ctx.mkExists"; + + static final String EX_CTX_MK_FORALL = "ctx.mkForall"; + + static final String EX_CTX_MK_SYMBOL = "ctx.mkSymbol"; + + static final String EX_CTX_MK_ITE = "ctx.mkITE"; + + static final String EX_CTX_MK_TRUE = "ctx.mkTrue()"; + + static final String EX_CTX_MK_FALSE = "ctx.mkFalse()"; + + static final String EX_INT_EXPR = "(IntExpr) "; + + static final String EX_BOOL_EXPR = "(BoolExpr) "; + + static final String EX_ARITH_EXPR = "(ArithExpr) "; + + static final String EX_ARRAY_EXPR_CATS = "(ArrayExpr) "; + + static final String EX_CTX_MK_BOOL_CONST = "ctx.mkBoolConst"; + + static final String EX_CTX_MK_INT_CONST = "ctx.mkIntConst"; + + static final String EX_CTX_MK_ARRAY_CONST = "ctx.mkArrayConst"; + + static final String AREA_LIST_NAME = "areaList"; + + static final String CONSTR_LIST_NAME = "constrList"; + + static final String CONSTR_LABEL_LIST_NAME = "constrLabelList"; + + static final String CONTENT_LIST_NAME = "contentList"; + + static final String CONTENT_LIST_ADD = "contentList.add"; + + static final String CONSTR_LIST_ADD = "constrList.add"; + + static final String AREA_LIST_ADD = "areaList.add"; + + static final String CONSTR_LABEL_LIST_ADD = "constrLabelList.add"; + + static final String VISIBILITY = " Visibility : "; + + static final String ZORDER = " Zorder : "; + + static final String GET = ".get"; + + static final String CONST_ADDED_VALUE = "10"; + + static final String STR_QUOTE = "\""; + + static final String _4SPACES = " "; + + static final String _8SPACES = " "; + + static final String OPEN = "("; + + static final String CLOSE = ")"; + + static final String NAME_SEPARATOR = "_"; + + static final String COMMA = ", "; + + static final String DOT = "."; + + static final String NULL_STRING = "null"; + + static final String SL_COMMENT = "//"; + + static final String NL = "\r\n"; + + static final String END = ";"; + + static final String NUMBER = "#"; + + static final String NUMBER_ZERO = "#0:"; + + static final String VARIABLE_CMT = "// Variable "; + + static final String VARIABLE_DEFINE = "Expr[] %s = new Expr[1];"; + + static final String VARIABLE_VAR_NAME = "variable_"; + + static final String AREASET_VAR_NAME = "areaSet_"; + + static final String ZONESET_VAR_NAME = "zoneSet_"; + + static final String VIEW_CONTENTSET_VAR_NAME = "vcontentSet_"; + + static final String SOUND_CONTENTSET_VAR_NAME = "scontentSet_"; + + static final String SETOF_OP_VAR_NAME = "setOfOperator_"; + + static final String ARRAY_TOP = "[0]"; + + static final String SET_VARIABLE_VALUE = " = ctx.mkConst(ctx.mkSymbol(\"%s\"), ctx.getIntSort());"; + + static final String OP_IS_DISPLAYED = "isDisplayed"; + + static final String OP_DISPLAYING_CONTENT = "displayingContent"; + + static final String OP_ALLOCATED_CONTENT = "allocatedContent"; + + static final String OP_CONTENTS_LIST = "contentsList"; + + static final String OP_IS_HIDDEN = "isHidden"; + + static final String OP_IS_ACTIVE = "isActive"; + + static final String OP_IS_VISIBLE = "isVisible"; + + static final String OP_ALLOCATABLE = "allocatable"; + + static final String OP_CONTENT_VALUE = "contentValue"; + + static final String OP_PRE_IS_DISPLAYED = "preIsDisplayed"; + + static final String OP_PRE_DISPLAYING_CONTENT = "preDisplayingContent"; + + static final String OP_PRE_ALLOCATED_CONTENT = "preAllocatedContent"; + + static final String OP_PRE_CONTENTS_LIST = "preContentsList"; + + static final String OP_PRE_IS_HIDDEN = "preIsHidden"; + + static final String OP_PRE_IS_ACTIVE = "preIsActive"; + + static final String OP_PRE_IS_VISIBLE = "preIsVisible"; + + static final String OP_PRE_ALLOCATABLE = "preAllocatable"; + + static final String OP_PRE_CONTENT_VALUE = "preContentValue"; + + static final String OP_IS_MUTED = "isMuted"; + + static final String OP_PRE_IS_MUTED = "preIsMuted"; + + static final String OP_IS_ATTENUATED = "isAttenuated"; + + static final String OP_PRE_IS_ATTENUATED = "preIsAttenuated"; + + static final String OP_IS_SOUNDING = "isSounding"; + + static final String OP_PRE_IS_SOUNDING = "preIsSounding"; + + static final String OP_OUTPUTTING_SOUND = "outputtingSound"; + + static final String OP_PRE_OUTPUTTING_SOUND = "preOutputtingSound"; + + static final String OP_IS_OUTPUTTED = "isOutputted"; + + static final String OP_PRE_IS_OUTPUTTED = "preIsOutputted"; + + static final String OP_GET_PROPERTY = "getProperty"; + + static final String OP_PRE_GET_PROPERTY = "preGetProperty"; + + static final String OP_IS_ON = "isOn"; + + static final String OP_PRE_IS_ON = "preIsOn"; + + static final String OP_IS_DEFEATED_BY = "isDefeatedBy"; + + static final String OP_PRE_IS_DEFEATED_BY = "preIsDefeatedBy\""; + + static final String OP_DEFEATS = "defeats"; + + static final String OP_PRE_DEFEATS = "preDefeats"; + + static final String OP_IS_DISAPPEARED = "isDisappeared"; + + static final String OP_PRE_IS_DISAPPEARED = "preIsDisappeared"; + + static final String OP_IS_CANCELED = "isCanceled"; + + static final String OP_PRE_IS_CANCELED = "preIsCanceled"; + + static final String OP_HAS_BEEN_DISPLAYED = "hasBeenDisplayed"; + + static final String OP_PRE_HAS_BEEN_DISPLAYED = "preHasBeenDisplayed"; + + static final String OP_HAS_COME_EARLIER_THAN = "hasComeEarlierThan"; + + static final String OP_HAS_COME_LATER_THAN = "hasComeLaterThan"; + + static final String OP_ACTIVE_CONTENTS = "activeContents"; + + static final String OP_PRE_ACTIVE_CONTENTS = "preActiveContents"; + + static final String EMP_ARRAY_CONST = "empArrayConst"; + + static final String ALL_AREA_CONST = "allInstanceOfAreaConst"; + + static final String ALL_ZONE_CONST = "allInstanceOfZoneConst"; + + static final String ALL_SOUNDCONTENT_CONST = "allInstanceOfSoundContentConst"; + + static final String ALL_VIEWCONTENT_CONST = "allInstanceOfViewContentConst"; + + static final String ALLOCATABLE_SIZE = "allocatableSize"; + + static final String CONTENT_SIZE = "contentSize"; + + static final String ARRAY_EXPR_SORT = "ArrayExpr "; + + static final String CONSTRAINT_PREFIX = "Constraint:"; + + static final String EQUAL = " = "; + + static final String INT_TYPE = "int_type"; + + static final String BOOL_TYPE = "bool_type"; + + static final String IMPLIES_CONSTRAINT_METHOD_NAME = "doCalculateImpliesConstraint_%s()"; + + static final String IMPLIES_CONSTRAINT_METHOD = "private List<String> %s {"; + + static final String IMPLIES_CONSTRAINT_METHOD_DETAIL1 = "List<String> constraint_%s" + EQUAL; + + static final String IMPLIES_CONSTRAINT_METHOD_DETAIL2 = "if(!constraint_%s.isEmpty() && !constraint_%s.get(0).equals(\"SAT\")) {"; + + static final String IMPLIES_CONSTRAINT_METHOD_DETAIL3 = "map.put(\"#%s:%s\", constraint_%s)"; + + static final String IMPLIES_CONSTRAINT_METHOD_DETAIL4 = "if(constraint_%s.get(0).equals(\"UNSAT\")) {"; + + static final String IMPLIES_CONSTRAINT_METHOD_DETAIL5 = "return map"; + + static final String BLOCK_CLOSE = "}"; + + static final String IF_OFFLINE = "if(!onlyOnline) {"; + + static final String STORE_TEMPLATE = EX_CTX_MK_STORE + OPEN + "%s" + COMMA + EX_CTX_MK_INT + OPEN + "%s" + CLOSE + COMMA + EX_CTX_MK_TRUE + CLOSE;; +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/z3/IConstraintGenerator.xtend b/rba.tool.editor/src/rba/tool/editor/generator/z3/IConstraintGenerator.xtend new file mode 100644 index 0000000..b1e01a9 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/z3/IConstraintGenerator.xtend @@ -0,0 +1,15 @@ +package rba.tool.editor.generator.z3 + +import org.eclipse.emf.ecore.resource.ResourceSet +import org.eclipse.xtext.generator.IFileSystemAccess2 +import org.eclipse.xtext.generator.IGenerator2 +import org.eclipse.xtext.generator.IGeneratorContext + +interface IConstraintGenerator extends IGenerator2 { + + def void doGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); + + def void beforeGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); + + def void afterGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); +}
\ No newline at end of file diff --git a/rba.tool.editor/src/rba/tool/editor/generator/z3/ISortValueGenerator.xtend b/rba.tool.editor/src/rba/tool/editor/generator/z3/ISortValueGenerator.xtend new file mode 100644 index 0000000..044ceae --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/z3/ISortValueGenerator.xtend @@ -0,0 +1,15 @@ +package rba.tool.editor.generator.z3 + +import org.eclipse.emf.ecore.resource.ResourceSet +import org.eclipse.xtext.generator.IFileSystemAccess2 +import org.eclipse.xtext.generator.IGenerator2 +import org.eclipse.xtext.generator.IGeneratorContext + +interface ISortValueGenerator extends IGenerator2 { + + def void doGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); + + def void beforeGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); + + def void afterGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context); +}
\ No newline at end of file diff --git a/rba.tool.editor/src/rba/tool/editor/generator/z3/SortValueCodeGenerationSupporter.java b/rba.tool.editor/src/rba/tool/editor/generator/z3/SortValueCodeGenerationSupporter.java new file mode 100644 index 0000000..b6e872a --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/z3/SortValueCodeGenerationSupporter.java @@ -0,0 +1,555 @@ +package rba.tool.editor.generator.z3; + +import java.util.ArrayList; +import java.util.List; +import java.util.function.Consumer; + +import org.eclipse.emf.common.util.EList; + +import rba.core.Allocatable; +import rba.core.ComparisonAnd; +import rba.core.ComparisonOperator; +import rba.core.Content; +import rba.core.ContentState; +import rba.core.EqualToOperator; +import rba.core.Expression; +import rba.core.GreaterThanOperator; +import rba.core.IfStatement; +import rba.core.IntegerValue; +import rba.core.LowerThanOperator; +import rba.core.MaxValue; +import rba.core.MinValue; +import rba.core.MuchGreaterThanOperator; +import rba.core.NoneValue; +import rba.core.ObjectReference; +import rba.core.Operator; +import rba.core.PlusOperator; +import rba.core.RuleObject; +import rba.core.StandardValue; +import rba.core.ThatOfOperator; +import rba.core.ValueExpression; +import rba.tool.editor.util.RBAModelEditorToolUtil; +import rba.view.Area; + +public class SortValueCodeGenerationSupporter implements GeneratorConstants { + + static final int LIST_LIMIT = 1000; + + static SortValueCodeTemplate template = new SortValueCodeTemplate(); + + private List<Area> areaList; + + private List<Allocatable> allocatableList; + + private List<Content> contentList; + + private List<ContentState> contentStateList; + + public String generate(List<Content> contents, List<Allocatable> allocatables, List<Area> areas) { + this.contentList = contents; + this.allocatableList = allocatables; + this.areaList = areas; + this.contentStateList = new ArrayList<ContentState>(); + + // for common + StringBuilder method_code_Adding = new StringBuilder(); + + // for calculateArea_zorder + StringBuilder area_zorder_code = new StringBuilder(); + StringBuilder areaListZorder_Adding = new StringBuilder(); + StringBuilder zorder_comment = new StringBuilder(); + StringBuilder zorderConstrList_Adding = new StringBuilder(); + StringBuilder areaConstrLabelListZorder_Adding = new StringBuilder(); + StringBuilder calculateArea_zorder_Method = new StringBuilder(); + List<StringBuilder> calculateAreaZorderMethidList = new ArrayList<StringBuilder>(); + + // for calculateAllocatable_visibility + StringBuilder allocatable_visibility_code = new StringBuilder(); + StringBuilder allocatableList_Adding = new StringBuilder(); + StringBuilder visibility_comment = new StringBuilder(); + StringBuilder visibilityConstrList_Adding = new StringBuilder(); + StringBuilder allocatableConstrLabelList_Adding = new StringBuilder(); + List<StringBuilder> calculateAllocatableVisibilityMethidList = new ArrayList<StringBuilder>(); + + // for calculateContentState_priority + StringBuilder content_state_priority_code = new StringBuilder(); + List<StringBuilder> contentStateMethidList = new ArrayList<StringBuilder>(); + StringBuilder content_state_priority_method_code = new StringBuilder(); + + area_zorder_code.append(_8SPACES + CMT_AREA_LIST + NL); + allocatable_visibility_code.append(_8SPACES + CMT_AREA_LIST + NL); + content_state_priority_code.append(_8SPACES + CMT_CONTENT_STATE_LIST + NL); + + /////////////////// Area/Zone Visibility Code Prepare @Start + List<List<Allocatable>> limitedAlloList = new ArrayList<>(); + ListHelper.extract(allocatableList, LIST_LIMIT, _list -> { + limitedAlloList.add(_list); + }); + + int visMethodNum = 0; + for (List<Allocatable> _list : limitedAlloList) { + method_code_Adding.append(getAllocatableVisibilityMethodString(_list, visMethodNum)); + allocatable_visibility_code.append(getAllocatableVisibilityMethodCallString(visMethodNum)); + visMethodNum++; + } + /////////////////// Area/Zone Visibility Code Prepare @End + + /////////////////// Area Zorder Code Prepare @Start + List<List<Area>> limitedAreaList = new ArrayList<>(); + ListHelper.extract(areaList, LIST_LIMIT, _list -> { + limitedAreaList.add(_list); + }); + + int zoMethodNum = 0; + for (List<Area> _list : limitedAreaList) { + method_code_Adding.append(getAreaZorderMethodString(_list, zoMethodNum)); + area_zorder_code.append(getAreaZorderMethodCallString(zoMethodNum)); + zoMethodNum++; + } + /////////////////// Area Zorder Code Prepare @End + + /////////////////// Content State Priority Code Prepare @Start + for (int i = 0; i < contentList.size(); i++) { + Content content = contentList.get(i); + for (ContentState cState : content.getStates()) { + contentStateList.add(cState); + } + } + List<List<ContentState>> limitedContentList = new ArrayList<>(); + ListHelper.extract(contentStateList, LIST_LIMIT, _list -> { + limitedContentList.add(_list); + }); + + int ctMethodNum = 0; + for (List<ContentState> _list : limitedContentList) { + method_code_Adding.append(getContentStateMethodString(_list, ctMethodNum)); + content_state_priority_code.append(getContentStateMethodCallString(ctMethodNum)); + ctMethodNum++; + } + + +// int num = 0; +// StringBuilder content_state_priority_code_main = new StringBuilder(); +// for (int i = 0; i < contentStateList.size(); i += LIST_LIMIT) { +// int toIdx = ((i + LIST_LIMIT) >= contentStateList.size() ? contentStateList.size() : (i + LIST_LIMIT)); +// StringBuilder contentStateMethod = getContentStateMethodString(contentStateList.subList(i, toIdx), num, content_state_priority_code_main); +// contentStateMethidList.add(contentStateMethod); +// num++; +// } +// +// content_state_priority_code.append(content_state_priority_code_main).append(NL); +// +// for (int j = 0; j < num; j++) { +// content_state_priority_code.append(_8SPACES + "createContentList" + j + "(contentList);" + NL); +// } +// for (int j = 0; j < num; j++) { +// content_state_priority_code.append(_8SPACES + "createConstrList" + j + "(contentList, constrList);" + NL); +// } +// for (int j = 0; j < num; j++) { +// content_state_priority_code.append(_8SPACES + "createConstrLabelList" + j + "(constrLabelList);" + NL); +// } +// for (StringBuilder method : contentStateMethidList) { +// method_code_Adding.append(method); +// } +// + /////////////////// Content State Priority Code Prepare @End + + template.area_zorder_code = area_zorder_code.toString(); + template.area_visibility_code = allocatable_visibility_code.toString(); + template.content_state_priority_code = content_state_priority_code.toString(); + template.method_code = method_code_Adding.toString(); + + // calculateAllocatableVisibilityMethidList + return template.getCompleteCode(); + } + + private String getContextString(Expression expression, int index, String listName, Class<?> clazz, Expression eContainer) { + String contextString = null; + if (expression instanceof MinValue) { + contextString = resolveExpression((MinValue) expression, index, listName, eContainer); + } else if (expression instanceof MaxValue) { + contextString = resolveExpression((MaxValue) expression, index, listName, eContainer); + } else if (expression instanceof StandardValue) { + contextString = resolveExpression((StandardValue) expression, index, listName, eContainer); + } else if (expression instanceof NoneValue) { + contextString = resolveExpression((NoneValue) expression, index, listName, eContainer); + } else if (expression instanceof IntegerValue) { + contextString = resolveExpression((IntegerValue) expression, index, listName, eContainer); + } else if (expression instanceof EqualToOperator) { + contextString = resolveExpression((EqualToOperator) expression, index, listName, clazz); + } else if (expression instanceof GreaterThanOperator) { + contextString = resolveExpression((GreaterThanOperator) expression, index, listName, clazz); + } else if (expression instanceof MuchGreaterThanOperator) { + contextString = resolveExpression((MuchGreaterThanOperator) expression, index, listName, clazz); + } else if (expression instanceof LowerThanOperator) { + contextString = resolveExpression((LowerThanOperator) expression, index, listName, clazz); + } else if (expression instanceof ThatOfOperator) { + contextString = resolveExpression((ThatOfOperator) expression, index, listName, clazz); + } else if (expression instanceof PlusOperator) { + contextString = resolveExpression((PlusOperator) expression, index, listName, clazz); + } else if (expression instanceof ComparisonAnd) { + contextString = resolveExpression((ComparisonAnd) expression, index, listName, clazz); + } else if (expression instanceof ObjectReference) { + contextString = resolveExpression((ObjectReference) expression, listName, clazz); + } else { + // TODO Specification not found + System.out.println("Expected Expression type is not supported yet!"); + } + return contextString; + } + + private StringBuilder getAllocatableVisibilityMethodCallString(int num) { + StringBuilder ret = new StringBuilder(); + ret.append(_8SPACES + FUNC_ALLO_LIST + num + OPEN + AREA_LIST_NAME + CLOSE + END + NL); + ret.append(_8SPACES + FUNC_ALLO_VIS_CONSTR + num + OPEN + AREA_LIST_NAME + COMMA + CONSTR_LIST_NAME + CLOSE + END + NL); + ret.append(_8SPACES + FUNC_ALLO_VIS_CONSTR_LBL + num + OPEN + CONSTR_LABEL_LIST_NAME + CLOSE + END + NL); + return ret; + } + + private StringBuilder getAllocatableVisibilityMethodString(List<Allocatable> allocatableLimitedList, int num) { + StringBuilder createAlloVisListMethod = new StringBuilder(); + String createAlloVisListMethodName = FUNC_ALLO_LIST + num; + StringBuilder createConstrListMethod = new StringBuilder(); + String createConstrListMethodName = FUNC_ALLO_VIS_CONSTR + num; + StringBuilder createConstrLabelListMethod = new StringBuilder(); + String createConstrLabelListMethodName = FUNC_ALLO_VIS_CONSTR_LBL + num; + + createAlloVisListMethod.append(_4SPACES + "private void " + createAlloVisListMethodName + "(List<Expr> " + AREA_LIST_NAME + ") {" + NL); + createConstrListMethod + .append(_4SPACES + "private void " + createConstrListMethodName + "(List<Expr> " + AREA_LIST_NAME + ", List<BoolExpr> " + CONSTR_LIST_NAME + ") {" + NL); + createConstrLabelListMethod.append(_4SPACES + "private void " + createConstrLabelListMethodName + "(List<BoolExpr> " + CONSTR_LABEL_LIST_NAME + ") {" + NL); + + int i = num * 1000; + for (Allocatable allocatable : allocatableLimitedList) { + /////////////////// Area List & Label List @Start + createAlloVisListMethod.append(_8SPACES + AREA_LIST_ADD + OPEN + EX_CTX_MK_INT_CONST + OPEN + STR_QUOTE + allocatable.getName() + STR_QUOTE + CLOSE + CLOSE + END + NL); + createConstrLabelListMethod + .append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + STR_QUOTE + allocatable.getName() + STR_QUOTE + CLOSE + CLOSE + END + NL); + + /////////////////// Area/Zone Visibility Code Prepare @Start + createConstrListMethod.append(_8SPACES + SL_COMMENT + allocatable.getName() + VISIBILITY + RBAModelEditorToolUtil.getExpressionText(allocatable.getVisibility()) + NL); + String visibilityContextString = getContextString(allocatable.getVisibility(), i, AREA_LIST_NAME, Allocatable.class, null); + if (visibilityContextString != null) { + createConstrListMethod.append(_8SPACES + CONSTR_LIST_ADD + OPEN + visibilityContextString + CLOSE + END + NL); + } + i++; + } + + createAlloVisListMethod.append(_4SPACES + "}" + NL + NL); + createConstrListMethod.append(_4SPACES + "}" + NL + NL); + createConstrLabelListMethod.append(_4SPACES + "}" + NL + NL); + + StringBuilder ret = new StringBuilder(); + ret.append(createAlloVisListMethod); + ret.append(createConstrListMethod); + ret.append(createConstrLabelListMethod); + + return ret; + } + + private StringBuilder getAreaZorderMethodCallString(int num) { + StringBuilder ret = new StringBuilder(); + ret.append(_8SPACES + FUNC_AREA_LIST + num + OPEN + AREA_LIST_NAME + CLOSE + END + NL); + ret.append(_8SPACES + FUNC_AREA_ZORDR_CONSTR + num + OPEN + AREA_LIST_NAME + COMMA + CONSTR_LIST_NAME + CLOSE + END + NL); + ret.append(_8SPACES + FUNC_AREA_ZORDR_CONSTR_LBL + num + OPEN + CONSTR_LABEL_LIST_NAME + CLOSE + END + NL); + return ret; + } + + private StringBuilder getAreaZorderMethodString(List<Area> areaLimitedList, int num) { + StringBuilder createAreaZodrListMethod = new StringBuilder(); + String createAreaZodrListMethodName = FUNC_AREA_LIST + num; + StringBuilder createConstrListMethod = new StringBuilder(); + String createConstrListMethodName = FUNC_AREA_ZORDR_CONSTR + num; + StringBuilder createConstrLabelListMethod = new StringBuilder(); + String createConstrLabelListMethodName = FUNC_AREA_ZORDR_CONSTR_LBL + num; + + createAreaZodrListMethod.append(_4SPACES + "private void " + createAreaZodrListMethodName + "(List<Expr> " + AREA_LIST_NAME + ") {" + NL); + createConstrListMethod + .append(_4SPACES + "private void " + createConstrListMethodName + "(List<Expr> " + AREA_LIST_NAME + ", List<BoolExpr> " + CONSTR_LIST_NAME + ") {" + NL); + createConstrLabelListMethod.append(_4SPACES + "private void " + createConstrLabelListMethodName + "(List<BoolExpr> " + CONSTR_LABEL_LIST_NAME + ") {" + NL); + + int i = num * 1000; + for (Area area : areaLimitedList) { + /////////////////// Area List & Label List @Start + createAreaZodrListMethod.append(_8SPACES + AREA_LIST_ADD + OPEN + EX_CTX_MK_INT_CONST + OPEN + STR_QUOTE + area.getName() + STR_QUOTE + CLOSE + CLOSE + END + NL); + createConstrLabelListMethod + .append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + STR_QUOTE + area.getName() + STR_QUOTE + CLOSE + CLOSE + END + NL); + + /////////////////// Area Zorder Code Prepare @Start + createConstrListMethod.append(_8SPACES + SL_COMMENT + area.getName() + ZORDER + RBAModelEditorToolUtil.getExpressionText(area.getZorder()) + NL); + String zorderContextString = getContextString(area.getZorder(), i, AREA_LIST_NAME, Area.class, null); + if (zorderContextString != null) { + createConstrListMethod.append(_8SPACES + CONSTR_LIST_ADD + OPEN + zorderContextString + CLOSE + END + NL); + } + i++; + } + + createAreaZodrListMethod.append(_4SPACES + "}" + NL + NL); + createConstrListMethod.append(_4SPACES + "}" + NL + NL); + createConstrLabelListMethod.append(_4SPACES + "}" + NL + NL); + + StringBuilder ret = new StringBuilder(); + ret.append(createAreaZodrListMethod); + ret.append(createConstrListMethod); + ret.append(createConstrLabelListMethod); + + return ret; + } + + private StringBuilder getContentStateMethodCallString(int num) { + StringBuilder ret = new StringBuilder(); + ret.append(_8SPACES + FUNC_CST_LIST + num + OPEN + CONTENT_LIST_NAME + CLOSE + END + NL); + ret.append(_8SPACES + FUNC_CST_CONSTR + num + OPEN + CONTENT_LIST_NAME + COMMA + CONSTR_LIST_NAME + CLOSE + END + NL); + ret.append(_8SPACES + FUNC_CST_CONSTR_LBL + num + OPEN + CONSTR_LABEL_LIST_NAME + CLOSE + END + NL); + return ret; + } + + private StringBuilder getContentStateMethodString(List<ContentState> contentStateLimitedList, int num) { + StringBuilder createContentListMethod = new StringBuilder(); + String createContentListMethodName = "createContentList" + num; + StringBuilder createConstrListMethod = new StringBuilder(); + String createConstrListMethodName = "createConstrList" + num; + StringBuilder createConstrLabelListMethod = new StringBuilder(); + String createConstrLabelListMethodName = "createConstrLabelList" + num; + + createContentListMethod.append(_4SPACES + "private void " + createContentListMethodName + "(List<Expr> contentList) {" + NL); + createConstrListMethod.append(_4SPACES + "private void " + createConstrListMethodName + "(List<Expr> contentList, List<BoolExpr> constrList) {" + NL); + createConstrLabelListMethod.append(_4SPACES + "private void " + createConstrLabelListMethodName + "(List<BoolExpr> constrLabelList) {" + NL); + + int i = num * 1000; + for (ContentState contentState: contentStateLimitedList) { + Content content = (Content) contentState.eContainer(); + String content_cState_Name = content.getName() + NAME_SEPARATOR + contentState.getName(); + + /////////////////// ContentState List & Label List @Start + createContentListMethod.append(_8SPACES + CONTENT_LIST_ADD + OPEN + EX_CTX_MK_INT_CONST + OPEN + STR_QUOTE + content_cState_Name + STR_QUOTE + CLOSE + CLOSE + END + NL); + createConstrLabelListMethod.append(_8SPACES + CONSTR_LABEL_LIST_ADD + OPEN + EX_CTX_MK_BOOL_CONST + OPEN + STR_QUOTE + content_cState_Name + STR_QUOTE + CLOSE + CLOSE + END + NL); + + /////////////////// ContentState Code Prepare @Start + createConstrListMethod.append(_8SPACES + SL_COMMENT + content_cState_Name + CMT_CONTENT_STATE_PRIORITY_COMMENT_CONNECTOR + CMT_NAME_OPEN + contentState.getValue().getExpression() + + CMT_NAME_CLOSE + NL); + String contentContextString = getContextString(contentState.getValue(), i, CONTENT_LIST_NAME, Content.class, null); + if (contentContextString != null) { + createConstrListMethod.append(_8SPACES + CONSTR_LIST_ADD + OPEN + contentContextString + CLOSE + END + NL); + } + i++; + } + + createContentListMethod.append(_4SPACES + "}" + NL); + createConstrListMethod.append(_4SPACES + "}" + NL); + createConstrLabelListMethod.append(_4SPACES + "}" + NL); + + StringBuilder ret = new StringBuilder(); + ret.append(createContentListMethod); + ret.append(createConstrListMethod); + ret.append(createConstrLabelListMethod); + + return ret; + } + + private String resolveExpression(MinValue expression, int index, String listName, Expression eContainer) { + if ((eContainer instanceof ComparisonOperator && !(eContainer instanceof ComparisonAnd)) || eContainer instanceof PlusOperator) { + return EX_MIN; + } + return EX_CTX_MK_EQ + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + EX_MIN + CLOSE; + } + + private String resolveExpression(MaxValue expression, int index, String listName, Expression eContainer) { + if ((eContainer instanceof ComparisonOperator && !(eContainer instanceof ComparisonAnd)) || eContainer instanceof PlusOperator) { + return EX_MAX; + } + return EX_CTX_MK_EQ + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + EX_MAX + CLOSE; + } + + private String resolveExpression(StandardValue expression, int index, String listName, Expression eContainer) { + if ((eContainer instanceof ComparisonOperator && !(eContainer instanceof ComparisonAnd)) || eContainer instanceof PlusOperator) { + return EX_STD; + } + return EX_CTX_MK_EQ + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + EX_STD + CLOSE; + } + + private String resolveExpression(NoneValue expression, int index, String listName, Expression eContainer) { + if ((eContainer instanceof ComparisonOperator && !(eContainer instanceof ComparisonAnd)) || eContainer instanceof PlusOperator) { + return EX_NON; + } + return EX_CTX_MK_EQ + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + EX_NON + CLOSE; + } + + private String resolveExpression(IntegerValue expression, int index, String listName, Expression eContainer) { + String context = null; + if ((eContainer instanceof ComparisonOperator && !(eContainer instanceof ComparisonAnd)) || eContainer instanceof PlusOperator) { + context = EX_INT_EXPR + EX_CTX_MK_INT + OPEN + ((IntegerValue) expression).getValue() + CLOSE; + } else if (eContainer == null) { + // TODO may be mismatch with specification. need confirmation + context = EX_CTX_MK_EQ + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + EX_INT_EXPR + EX_CTX_MK_INT + OPEN + ((IntegerValue) expression).getValue() + + CLOSE + CLOSE; + } else { + // TODO may be new feature that was not specified yet for SortValueGeneration + System.out.println("Not supported yet."); + } + return context; + } + + private String resolveExpression(EqualToOperator expression, int index, String listName, Class<?> clazz) { + EList<Expression> operand = ((EqualToOperator) expression).getOperand(); + String context = null; + if (operand.get(0) instanceof Operator) { + context = getContextString(operand.get(0), index, listName, clazz, expression); + } else if (operand.get(0) instanceof ObjectReference) { + context = resolveExpression((ObjectReference) operand.get(0), listName, clazz); + } else if (operand.get(0) instanceof ValueExpression) { + // TODO To confirm, specification not found + context = getContextString(operand.get(0), index, listName, clazz, expression); + } else if (operand.get(0) instanceof IfStatement) { + // TODO To confirm, specification not found + System.out.println("Not supported yet"); + } + context = (context == null) ? null : EX_CTX_MK_EQ + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + context + CLOSE; + return context; + } + + private String resolveExpression(GreaterThanOperator expression, int index, String listName, Class<?> clazz) { + EList<Expression> operand = ((GreaterThanOperator) expression).getOperand(); + String context = null; + if (operand.get(0) instanceof Operator) { + context = getContextString(operand.get(0), index, listName, clazz, expression); + } else if (operand.get(0) instanceof ObjectReference) { + context = resolveExpression((ObjectReference) operand.get(0), listName, clazz); + } else if (operand.get(0) instanceof ValueExpression) { + // TODO To confirm, specification not found + context = getContextString(operand.get(0), index, listName, clazz, expression); + } else if (operand.get(0) instanceof IfStatement) { + // TODO To confirm, specification not found + } + context = (context == null) ? null : EX_CTX_MK_GT + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + context + CLOSE; + return context; + } + + private String resolveExpression(MuchGreaterThanOperator expression, int index, String listName, Class<?> clazz) { + EList<Expression> operand = ((MuchGreaterThanOperator) expression).getOperand(); + String context = null; + if (operand.get(0) instanceof Operator) { + context = getContextString(operand.get(0), index, listName, clazz, expression); + } else if (operand.get(0) instanceof ObjectReference) { + context = resolveExpression((ObjectReference) operand.get(0), listName, clazz); + } else if (operand.get(0) instanceof ValueExpression) { + // TODO To confirm, specification not found + context = getContextString(operand.get(0), index, listName, clazz, expression); + } else if (operand.get(0) instanceof IfStatement) { + // TODO To confirm, specification not found + } + context = (context == null) ? null + : EX_CTX_MK_GT + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + EX_INT_EXPR + EX_CTX_MK_ADD + OPEN + context + COMMA + EX_CTX_MK_INT + OPEN + + CONST_ADDED_VALUE + CLOSE + CLOSE + CLOSE; + return context; + } + + private String resolveExpression(LowerThanOperator expression, int index, String listName, Class<?> clazz) { + EList<Expression> operand = ((LowerThanOperator) expression).getOperand(); + String context = null; + if (operand.get(0) instanceof Operator) { + context = getContextString(operand.get(0), index, listName, clazz, expression); + } else if (operand.get(0) instanceof ObjectReference) { + context = resolveExpression((ObjectReference) operand.get(0), listName, clazz); + } else if (operand.get(0) instanceof ValueExpression) { + // TODO To confirm, specification not found + context = getContextString(operand.get(0), index, listName, clazz, expression); + } else if (operand.get(0) instanceof IfStatement) { + // TODO To confirm, specification not found + } + context = (context == null) ? null : EX_CTX_MK_LT + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + context + CLOSE; + return context; + } + + private String resolveExpression(ThatOfOperator expression, int index, String listName, Class<?> clazz) { + EList<Expression> operand = ((ThatOfOperator) expression).getOperand(); + if (operand.get(0) instanceof ObjectReference) { + if (expression.eContainer() instanceof RuleObject) { // Area, Content + return EX_CTX_MK_EQ + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + resolveExpression((ObjectReference) operand.get(0), listName, clazz) + CLOSE; + } else { + return resolveExpression((ObjectReference) operand.get(0), listName, clazz); + } + } + return null; + } + + private String resolveExpression(ObjectReference expression, String listName, Class<?> clazz) { + if ((clazz == Allocatable.class && expression.getRefObject() instanceof Allocatable)) { + return EX_INT_EXPR + getListString(listName, allocatableList.indexOf(expression.getRefObject())); + } else if ((clazz == Area.class && expression.getRefObject() instanceof Area)) { + return EX_INT_EXPR + getListString(listName, areaList.indexOf(expression.getRefObject())); + } else if ((clazz == Content.class && expression.getRefObject() instanceof ContentState)) { + return EX_INT_EXPR + getListString(listName, contentStateList.indexOf(expression.getRefObject())); + } + return null; + } + + private String resolveExpression(PlusOperator expression, int index, String listName, Class<?> clazz) { + EList<Expression> operand = ((PlusOperator) expression).getOperand(); + StringBuilder builder = new StringBuilder(); + StringBuilder context = new StringBuilder(); + String operandContext = null; + + for (int i = 0; i < operand.size(); i++) { + if (i != 0) { + builder.append(EX_CTX_MK_ADD); + builder.append(OPEN); + context.append(COMMA); + if ((operandContext = getContextString(operand.get(i), index, listName, clazz, expression)) == null) { + return null; + } + context.append(operandContext); + context.append(CLOSE); + } else { + if ((operandContext = getContextString(operand.get(i), index, listName, clazz, expression)) == null) { + return null; + } + context.append(operandContext); + } + } + builder.append(context); + if (expression.eContainer() instanceof RuleObject) { // Area, Content + return EX_CTX_MK_EQ + OPEN + EX_INT_EXPR + getListString(listName, index) + COMMA + builder.toString() + CLOSE; + } else { + return builder.toString(); + } + } + + private String resolveExpression(ComparisonAnd expression, int index, String listName, Class<?> clazz) { + EList<Expression> operand = ((ComparisonAnd) expression).getOperand(); + if (operand.size() >= 2) { + StringBuilder beginContext = new StringBuilder(); + StringBuilder endContext = new StringBuilder(); + for (int i = 0; i < operand.size(); i++) { + String context = getContextString(operand.get(i), index, listName, clazz, null); + if (i == 0) { + beginContext.append(EX_CTX_MK_AND + OPEN); + endContext.append(context); + } else if (i == operand.size() - 1) { + endContext.append(COMMA).append(" ") // Include space or not, it is ok + .append(context).append(CLOSE); + } else { + beginContext.append(EX_CTX_MK_AND + OPEN); + endContext.append(COMMA).append(" ") // Include space or not, it is ok + .append(context).append(CLOSE); + } + } + return beginContext.toString() + endContext.toString(); + } + return null; // It may be rba model problem. + } + + private String getListString(String listName, int index) { + return listName + GET + OPEN + index + CLOSE; + } + + private interface ListHelper<T> extends Iterable<T> { + + public static <T> void extract(List<T> list, int size, Consumer<? super List<T>> bulkList) { + for (int i = 0; i < list.size(); i += size) { + List<T> _list = new ArrayList<>(list.subList(i, Integer.min(i + size, list.size()))); + bulkList.accept(_list); + } + } + } +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/z3/SortValueCodeTemplate.java b/rba.tool.editor/src/rba/tool/editor/generator/z3/SortValueCodeTemplate.java new file mode 100644 index 0000000..011c684 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/z3/SortValueCodeTemplate.java @@ -0,0 +1,148 @@ +package rba.tool.editor.generator.z3; + +public class SortValueCodeTemplate { + + String area_zorder_code; + + String area_visibility_code; + + String content_state_priority_code; + + String method_code; + + private static final String NL = "\r\n"; + + String getCompleteCode() { + return "import groovy.transform.CompileStatic;" + NL + NL + + "import java.util.ArrayList;" + NL + + "import java.util.HashMap;" + NL + + "import java.util.List;" + NL + + "import java.util.Map;" + NL + NL + + + "import com.microsoft.z3.BoolExpr;" + NL + + "import com.microsoft.z3.Context;" + NL + + "import com.microsoft.z3.Expr;" + NL + + "import com.microsoft.z3.IntExpr;" + NL + + "import com.microsoft.z3.Solver;" + NL + + "import com.microsoft.z3.Status;" + NL + NL + + + "import rba.tool.core.z3.Z3CodeManager;" + NL + NL + + + "@CompileStatic" + NL + + "public class SortValueCalculation implements rba.tool.core.sort.ISortValueCalculation {" + NL + NL + + " Context ctx;" + NL + + " IntExpr std;" + NL + + " IntExpr min;" + NL + + " IntExpr max;" + NL + + " IntExpr non;" + NL + NL + + " BoolExpr stdConstr;" + NL + + " BoolExpr minConstr;" + NL + + " BoolExpr maxConstr;" + NL + + " BoolExpr nonConstr;" + NL + NL + + + " public void setUp() {" + NL + + " ctx = new Context();" + NL + + " std = ctx.mkIntConst(\"STANDARD\");" + NL + + " stdConstr = ctx.mkEq(std, ctx.mkInt(10));" + NL + NL + + + " min = ctx.mkIntConst(\"MIN_VALUE\");" + NL + + " minConstr = ctx.mkEq(min, ctx.mkInt(0));" + NL + NL + + + " max = ctx.mkIntConst(\"MAX_VALUE\");" + NL + + " maxConstr = ctx.mkEq(max, ctx.mkInt(9999));" + NL + NL + + + " non = ctx.mkIntConst(\"NONE_VALUE\");" + NL + + " nonConstr = ctx.mkEq(non, ctx.mkInt(-1));" + NL + + " }" + NL + NL + + " public void close() {" + NL + + " ctx.close();" + NL + + " }" + NL + NL + + + " /**" + NL + + " * Derived the value of Zorder" + NL + + " */" + NL + + " public Map<String, Integer> calculateArea_zorder() {" + NL + + " Solver s = ctx.mkSolver();" + NL + + " s.push();" + NL + NL + + " List<Expr> areaList = new ArrayList<Expr>();" + NL + + " List<BoolExpr> constrList = new ArrayList<BoolExpr>();" + NL + + " List<BoolExpr> constrLabelList = new ArrayList<BoolExpr>();" + NL + NL + + + area_zorder_code + NL + + + " s.add(stdConstr);" + NL + + " s.add(minConstr);" + NL + + " s.add(maxConstr);" + NL + + " s.add(nonConstr);" + NL + NL + + + " for (int i = 0; i < constrList.size(); i++) {" + NL + + " s.assertAndTrack(constrList.get(i), constrLabelList.get(i));" + NL + + " }" + NL + NL + + " Status st = s.check();" + NL + + " Map<String, Integer> map = Z3CodeManager.INSTNACE.setModel(s, areaList, st);" + NL + + " s.pop();" + NL + + " return map;" + NL + + " }" + NL + NL + + + " /**" + NL + + " * Derivation of Visibility value" + NL + + " */" + NL + + " public Map<String, Integer> calculateAllocatable_visibility() {" + NL + + " Solver s = ctx.mkSolver();" + NL + + " s.push();" + NL + NL + + + " List<Expr> areaList = new ArrayList<Expr>();" + NL + + " List<BoolExpr> constrList = new ArrayList<BoolExpr>();" + NL + + " List<BoolExpr> constrLabelList = new ArrayList<BoolExpr>();" + NL + NL + + + area_visibility_code + NL + + + " s.add(stdConstr);" + NL + + " s.add(minConstr);" + NL + + " s.add(maxConstr);" + NL + + " s.add(nonConstr);" + NL + NL + + + " for (int i = 0; i < constrList.size(); i++) {" + NL + + " s.assertAndTrack(constrList.get(i), constrLabelList.get(i));" + NL + + " }" + NL + NL + + + " Status st = s.check();" + NL + + " Map<String, Integer> map = Z3CodeManager.INSTNACE.setModel(s, areaList, st); \r\n" + NL + + " s.pop();" + NL + + " return map;" + NL + + " }" + NL + NL + + + " /**" + NL + + " * Derived the value of priority" + NL + + " */" + NL + + " public Map<String, Integer> calculateContentState_priority() {" + NL + + " Solver s = ctx.mkSolver();" + NL + + " s.push();" + NL + NL + + + " List<Expr> contentList = new ArrayList<Expr>();" + NL + + " List<BoolExpr> constrList = new ArrayList<BoolExpr>();" + NL + + " List<BoolExpr> constrLabelList = new ArrayList<BoolExpr>();" + NL + NL + + + content_state_priority_code + NL + + + " s.add(stdConstr);" + NL + + " s.add(minConstr);" + NL + + " s.add(maxConstr);" + NL + + " s.add(nonConstr);" + NL + NL + + + " for (int i = 0; i < constrList.size(); i++) {" + NL + + " s.assertAndTrack(constrList.get(i), constrLabelList.get(i));" + NL + + " }" + NL + NL + + + " Status st = s.check();" + NL + + " Map<String, Integer> map = Z3CodeManager.INSTNACE.setModel(s, contentList, st);" + NL + + " s.pop();" + NL + + " return map;" + NL + + " }" + NL + + + method_code + NL + + + + "}" + NL; + } +} diff --git a/rba.tool.editor/src/rba/tool/editor/generator/z3/SortValueGeneratorImpl.xtend b/rba.tool.editor/src/rba/tool/editor/generator/z3/SortValueGeneratorImpl.xtend new file mode 100644 index 0000000..0ef3691 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/z3/SortValueGeneratorImpl.xtend @@ -0,0 +1,46 @@ +package rba.tool.editor.generator.z3 + +import org.eclipse.emf.ecore.resource.Resource +import org.eclipse.emf.ecore.resource.ResourceSet +import org.eclipse.xtext.generator.AbstractGenerator +import org.eclipse.xtext.generator.IFileSystemAccess2 +import org.eclipse.xtext.generator.IGeneratorContext +import rba.tool.editor.model.manager.ResourceManager + +/** + * Generates code from your model files on save. + * + * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#code-generation + */ +class SortValueGeneratorImpl extends AbstractGenerator implements ISortValueGenerator { + + private static SortValueCodeGenerationSupporter generationSupporter = new SortValueCodeGenerationSupporter(); + + override doGenerate(Resource input, IFileSystemAccess2 fsa, IGeneratorContext context) { + doGenerate(input.resourceSet, fsa, context); + } + + override beforeGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + } + + override afterGenerate(ResourceSet input, IFileSystemAccess2 fsa, IGeneratorContext context) { + } + + override void doGenerate(ResourceSet resourceSet, IFileSystemAccess2 fsa, IGeneratorContext context) { + fsa.generateFile("SortValueCalculation.java", resourceSet.compile); + } + + def compile(ResourceSet resourceSet) ''' + «val allAllocatables = ResourceManager.INSTANCE.getRbaAllocatables(resourceSet)» + + «val allAreas = ResourceManager.INSTANCE.getRbaAreas(resourceSet)» +««« «FOR area : allAreas» +««« «area.name» : [ «FOR content : area.contents»«content.name», «ENDFOR»] +««« «ENDFOR» + «val allContents = ResourceManager.INSTANCE.getRbaContents(resourceSet)» +««« «FOR content : allContents» +««« «content.name» : [ «FOR area : content.allocatable»«area.name», «ENDFOR»] +««« «ENDFOR» + «generationSupporter.generate(allContents, allAllocatables, allAreas)» + ''' +} |