diff options
Diffstat (limited to 'rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintCodeGenerationSupporter.java')
| -rw-r--r-- | rba.tool.editor/src/rba/tool/editor/generator/z3/ConstraintCodeGenerationSupporter.java | 1599 |
1 files changed, 1599 insertions, 0 deletions
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; + } + } +} |