From c1ee09e4925ecd6c7220926fabc3581ba3183456 Mon Sep 17 00:00:00 2001 From: Pedro Ribeiro Date: Tue, 18 Jun 2024 11:53:12 +0100 Subject: [PATCH] Squashed 'sleec-core/' changes from a42491f..9350f48 9350f48 Merge pull request #6 from SLEEC-project/fix-regeneration c0cdb8f Commented out built-in checks for conflicts. 84203e0 Fixed (re)-generation of instantiations + tick-tock. git-subtree-dir: sleec-core git-subtree-split: 9350f487fd873d43e6580a917b5cb1768962efbe --- .../robocalc/sleec/SLEECRuntimeModule.xtend | 6 + .../robocalc/sleec/generator/Main.xtend | 12 + .../sleec/generator/SLEECGenerator.xtend | 55 ++-- .../SLEECOutputConfigurationProvider.xtend | 25 ++ .../sleec/validation/SLEECValidator.xtend | 298 +++++++++--------- 5 files changed, 224 insertions(+), 172 deletions(-) create mode 100644 circus.robocalc.sleec/src/circus/robocalc/sleec/generator/SLEECOutputConfigurationProvider.xtend diff --git a/circus.robocalc.sleec/src/circus/robocalc/sleec/SLEECRuntimeModule.xtend b/circus.robocalc.sleec/src/circus/robocalc/sleec/SLEECRuntimeModule.xtend index 38b2715..8094d1b 100644 --- a/circus.robocalc.sleec/src/circus/robocalc/sleec/SLEECRuntimeModule.xtend +++ b/circus.robocalc.sleec/src/circus/robocalc/sleec/SLEECRuntimeModule.xtend @@ -14,9 +14,15 @@ ********************************************************************************/ package circus.robocalc.sleec +import org.eclipse.xtext.generator.IOutputConfigurationProvider +import circus.robocalc.sleec.generator.SLEECOutputConfigurationProvider /** * Use this class to register components to be used at runtime / without the Equinox extension registry. */ class SLEECRuntimeModule extends AbstractSLEECRuntimeModule { + + def Class bindIOutputConfigurationProvider() { + return SLEECOutputConfigurationProvider + } } diff --git a/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/Main.xtend b/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/Main.xtend index 7466dec..22362ea 100644 --- a/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/Main.xtend +++ b/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/Main.xtend @@ -26,6 +26,7 @@ import org.eclipse.xtext.util.CancelIndicator import org.eclipse.xtext.validation.CheckMode import org.eclipse.xtext.validation.IResourceValidator import org.eclipse.xtext.diagnostics.Severity +import org.eclipse.xtext.generator.OutputConfiguration class Main { @@ -62,6 +63,17 @@ class Main { // Configure and start the generator if there were no errors fileAccess.outputPath = 'src-gen/' + val dc = new OutputConfiguration("circus.robocalc.sleec"); + dc.setDescription("Configuration for SLEEC generator"); + dc.setOutputDirectory("src-gen"); + dc.setOverrideExistingResources(true); + dc.setCreateOutputDirectory(true); + dc.setCanClearOutputDirectory(true); + dc.setCleanUpDerivedResources(false); + dc.setSetDerivedProperty(true); + dc.setKeepLocalHistory(true); + fileAccess.outputConfigurations.put(dc.name, dc) + val context = new GeneratorContext => [ cancelIndicator = CancelIndicator.NullImpl ] diff --git a/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/SLEECGenerator.xtend b/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/SLEECGenerator.xtend index 63db885..2a24cdc 100644 --- a/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/SLEECGenerator.xtend +++ b/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/SLEECGenerator.xtend @@ -48,6 +48,8 @@ import java.util.HashSet import java.io.File import circus.robocalc.sleec.sLEEC.Constraint import java.util.LinkedHashSet +import org.eclipse.core.runtime.FileLocator +import java.net.URL /** * Generates code from your model files on save. @@ -58,22 +60,22 @@ class SLEECGenerator extends AbstractGenerator { Set scaleIDs Set measureIDs + + static final String GEN_ID = "circus.robocalc.sleec" override void doGenerate(Resource resource, IFileSystemAccess2 fsa, IGeneratorContext context) { this.scaleIDs = resource.allContents.filter(Measure).filter[it.type instanceof Scale].map['v' + it.name].toSet this.measureIDs = resource.allContents.filter(Measure).map[name].toSet - - val ticktock = new File("../src-gen/ticktock.csp") - if (!ticktock.exists()) { + + if (!fsa.isFile('tick-tock.csp', GEN_ID)) { generateTickTock(resource, fsa, context) } - val instantiatons = new File("../src-gen/ticktock.csp") - if (!instantiatons.exists()) { + if (!fsa.isFile('instantiations.csp', GEN_ID)) { generateInstantiations(resource, fsa, context) } - fsa.generateFile(resource.getURI().trimFileExtension().lastSegment() + '.csp', ''' + fsa.generateFile(resource.getURI().trimFileExtension().lastSegment() + '.csp', GEN_ID, ''' --Specify the integer intervals for type Int e.g. {0..30}. @@ -112,7 +114,7 @@ class SLEECGenerator extends AbstractGenerator { } ''') - fsa.generateFile(resource.getURI().trimFileExtension().lastSegment() + '-assertions.csp', ''' + fsa.generateFile(resource.getURI().trimFileExtension().lastSegment() + '-assertions.csp', GEN_ID, ''' -- ASSERTIONS -- include "tick-tock.csp" include "instantiations.csp" @@ -488,7 +490,8 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir var assertions = '' var assertions_part = '' if (unionMeasures.size == 0) { - assertions += ''' «firstRule.name»_wrt_«secondRule.name» = + assertions += ''' + «firstRule.name»_wrt_«secondRule.name» = let -- The external 'm' channels for every measure of («firstRule.name» or «secondRule.name») MemoryExternalEvents = {||} @@ -519,7 +522,8 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir ''' }else if (unionMeasures.size == 1) { val element = unionMeasures.get(0) - assertions += ''' «firstRule.name»_wrt_«secondRule.name» = + assertions += ''' + «firstRule.name»_wrt_«secondRule.name» = let -- The external 'm' channels for every measure of («firstRule.name» or «secondRule.name») MemoryExternalEvents = {|«element»|} @@ -555,7 +559,8 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir }else{ // (unionMeasures.size >1) - assertions += ''' «firstRule.name»_wrt_«secondRule.name» = + assertions += ''' + «firstRule.name»_wrt_«secondRule.name» = let -- The external 'm' channels for every measure of («firstRule.name» or «secondRule.name») MemoryExternalEvents = {|''' @@ -569,8 +574,9 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir } } assertions+='''|}''' - assertions+=''' -- The internal 'i_m' channels for every measure of («firstRule.name» or «secondRule.name») - MemoryInternalEvents = {|''' + assertions+=''' + -- The internal 'i_m' channels for every measure of («firstRule.name» or «secondRule.name») + MemoryInternalEvents = {|''' for (m : 0 ..< unionMeasures.size) { val element = unionMeasures.get(m) @@ -624,7 +630,8 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir assertions+= '''-> MemoryInOrder ''' - assertions+= '''within + assertions+= ''' + within timed_priority( ( ( @@ -637,12 +644,15 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir } else if (m > 0) { - assertions += ''', - «element» <- i_«element» + assertions += + ''' + , + «element» <- i_«element» ''' } } - assertions += ''' ]] + assertions += ''' + ]] ) [| union(diff(A«firstRule.name»,MemoryExternalEvents),MemoryInternalEvents) |] ( @@ -652,7 +662,7 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir MemoryInOrder ) ) \MemoryInternalEvents - ) + ) ''' } } @@ -883,7 +893,7 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir } private def generateInstantiations(Resource resource, IFileSystemAccess2 fsa, IGeneratorContext context) { - fsa.generateFile('instantiations.csp', + fsa.generateFile('instantiations.csp', GEN_ID, ''' -- This file contains user-adjustable parameters for model-checking. @@ -898,8 +908,9 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir // ----------------------------------------------------------- private def generateTickTock(Resource resource, IFileSystemAccess2 fsa, IGeneratorContext context) { fsa.generateFile( - 'tick-tock.csp', - '''--------------------------------------------------------------------------- + 'tick-tock.csp', GEN_ID, + ''' + --------------------------------------------------------------------------- -- Pedro Ribeiro -- Department of Computer Science -- University of York @@ -1260,9 +1271,7 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir endmodule --------------------------------------------------------------------------- - - - ''' + ''' ) } diff --git a/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/SLEECOutputConfigurationProvider.xtend b/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/SLEECOutputConfigurationProvider.xtend new file mode 100644 index 0000000..3661bfb --- /dev/null +++ b/circus.robocalc.sleec/src/circus/robocalc/sleec/generator/SLEECOutputConfigurationProvider.xtend @@ -0,0 +1,25 @@ +package circus.robocalc.sleec.generator + +import org.eclipse.xtext.generator.OutputConfigurationProvider +import org.eclipse.xtext.generator.OutputConfiguration +import java.util.HashSet + +class SLEECOutputConfigurationProvider extends OutputConfigurationProvider { + + override getOutputConfigurations() { + + var ocp = new HashSet// super.getOutputConfigurations() + val dc = new OutputConfiguration("circus.robocalc.sleec"); + dc.setDescription("Configuration for SLEEC generator"); + dc.setOutputDirectory("src-gen"); + dc.setOverrideExistingResources(true); + dc.setCreateOutputDirectory(true); + dc.setCanClearOutputDirectory(true); + dc.setCleanUpDerivedResources(false); + dc.setSetDerivedProperty(true); + dc.setKeepLocalHistory(true); + ocp.add(dc) + return ocp + + } +} \ No newline at end of file diff --git a/circus.robocalc.sleec/src/circus/robocalc/sleec/validation/SLEECValidator.xtend b/circus.robocalc.sleec/src/circus/robocalc/sleec/validation/SLEECValidator.xtend index d7f4bb9..c5d6ddd 100644 --- a/circus.robocalc.sleec/src/circus/robocalc/sleec/validation/SLEECValidator.xtend +++ b/circus.robocalc.sleec/src/circus/robocalc/sleec/validation/SLEECValidator.xtend @@ -135,155 +135,155 @@ class SLEECValidator extends AbstractSLEECValidator { // check for conflicts - // create map between each variable and the expressions that it is found in - val Multimap expressions = HashMultimap.create() - ruleBlock.eAllContents - .filter(MBoolExpr) - .forEach[ expr | - switch(expr) { - Atom case system.isBoolean(expr.measureID): - expressions.put(expr.measureID, null) - RelComp: { - val args = expr.eContents - .filter(Atom) - .map[measureID] - .filter[system.isNumeric(it) || system.isScaleID(it)] - // TODO also include expressions that contain two variables as its arguments - // but this checking for conflicts is more difficult e.g. x < y, y < z, x < y - args.length == 1 ? expressions.put(args.get(0), expr) - } - } - ] -// System.out.println('variable -> expression:\t' + expressions) - - // find possible values for each variable to make each expression either true or false - // for numeric expressions x = 5, x < 3, x > 7 the values of x can be: 0, 5, 10 - // for any boolean expression b: b will be 0 (false), 1 (true) - // for any scale expression: the values will be the 0 .. #scaleParams - 1 - val Multimap values = HashMultimap.create() - expressions.asMap.forEach [ k, v | - switch(k) { - case system.isBoolean(k): - values.get(k).addAll(0, 1) - case system.isNumeric(k): { - val getValue = [ RelComp expr | - system.eval(expr.left) ?: system.eval(expr.right) - ] - val range = v.map(getValue).min - 1 .. v.map(getValue).max + 1 - val Set> outcomes = new HashSet() - values.putAll(k, range.filter [ i | - val result = v.map [ expr | - val left = system.eval(expr.left) ?: i - val right = system.eval(expr.right) ?: i - SLEECEvaluator.eval(left, expr.op, right) - ].toList - outcomes.add(result) - ]) - } - case system.isScaleID(k): { - val eval = [ MBoolExpr expr | - switch (expr) { - Atom: system.scales.get(k).indexOf(expr.measureID) - } - ] - val range = 0 ..< system.scales.get(k).length - val Set> outcomes = new HashSet() - values.putAll(k, range.filter [ i | - val result = v.map [ expr | - val Integer left = eval.apply(expr.left) ?: i - val Integer right = eval.apply(expr.right) ?: i - SLEECEvaluator.eval(left, expr.op, right) - ].toList - outcomes.add(result) - ]) - } - } - ] -// System.out.println('variable -> value:\t' + values) - - // map between a rule and the index of the index of the combination of values of variables if that combination triggered the rule - // for: - // Rule0 when Event0 and x = 5 or y = 3 then E1 - // Rule1 when Event0 and x = 3 and y = 6 then E1 - // values will be - //{x = [x = 5, x = 3], y = [y = 3, y = 6]} - // the cartesian product of the values will be: - // {[x = 5, y = 3], [x = 5, y = 6], [x = 3, y = 3], [x = 3, y = 6]} - // ruleeTriggered will be: - // {Rule0 = [0, 1, 2], Rule1 = [3]} - val Multimap ruleTriggered = HashMultimap.create() - Sets.cartesianProduct(values.asMap.values.map[toSet]).forEach [ combination, i | - val variables = (0 ..< combination.size).toMap([values.keySet.get(it)], [combination.get(it)]) - val scales = new HashMap() - system.scales.values.forEach [ - forEach[k, v|scales.put(k, v)] - ] -// System.out.println(variables) - val evaluator = new SLEECEvaluator(variables, system.constants, scales) - ruleBlock.rules.forEach [ rule | - evaluator.eval(rule) ? ruleTriggered.put(rule, i) - ] - ] -// System.out.println('expressions:\t' + expressions.values.length + '\t' + expressions.values.join(' ')) -// System.out.println('rule -> triggered?\t' + ruleTriggered) - - // group rules by matching trigger-response pair - val Multimap, Rule> rules = HashMultimap.create() - ruleBlock.rules.forEach [ rule | - rules.put(rule.trigger.event.name -> rule.response.constraint.event.name, rule) - ] -// System.out.println('trigger -> response:\t' + rules) - - // check for conflicts and redundancies - rules.asMap.forEach [ trigger, triggeredRules | - for (i : 0 ..< triggeredRules.length){ - - val rule0 = triggeredRules.get(i) - val set0 = ruleTriggered.get(rule0) - - for (j : i + 1 ..< triggeredRules.length) { - - val rule1 = triggeredRules.get(j) - val set1 = ruleTriggered.get(rule1) - // first check for conflicts - // conflicts happen when responses in the form are both triggered at the same time - // Event0 within x - // not Event0 within y - // where y < x - if (rule0.response.constraint.not != rule1.response.constraint.not) { - // only 1 of the 2 rules has a not in their response - if (rule0.response.constraint.not && system.eval(rule0.response.constraint.value) < system.eval(rule1.response.constraint.value) || - rule1.response.constraint.not && system.eval(rule0.response.constraint.value) > system.eval(rule1.response.constraint.value)) { - error('''«rule0.name» conflicts with «rule1.name».''', rule0, SLEECPackage.Literals.RULE__NAME) - error('''«rule1.name» conflicts with «rule0.name».''', rule1, SLEECPackage.Literals.RULE__NAME) - return - } - - } - // then check for redundancies - else { - // either both rules have 'not' or don't have 'not' - val rule0Redundant = set1.containsAll(set0) - val rule1Redundant = set0.containsAll(set1) - // rule0 is redundant if result == 1 - // rule1 is redundant is result == -1 - // no rules are redundant if result == 0 - var result = - if (rule0Redundant && (!rule1Redundant || system.eval(rule0.response.constraint.value) <= system.eval(rule1.response.constraint.value))) - 1 - else if (rule1Redundant) - -1 - // if both rules have not, invert the result - rule0.response.constraint.not && rule1.response.constraint.not ? result = -result - switch (result) { - case 1: warning('''Redundant rule: «rule0.name», under «rule1.name».''', rule0, SLEECPackage.Literals.RULE__NAME) - case -1: warning('''Redundant rule: «rule1.name», under «rule0.name».''', rule1, SLEECPackage.Literals.RULE__NAME) - } - } - } - } - ] - +// // create map between each variable and the expressions that it is found in +// val Multimap expressions = HashMultimap.create() +// ruleBlock.eAllContents +// .filter(MBoolExpr) +// .forEach[ expr | +// switch(expr) { +// Atom case system.isBoolean(expr.measureID): +// expressions.put(expr.measureID, null) +// RelComp: { +// val args = expr.eContents +// .filter(Atom) +// .map[measureID] +// .filter[system.isNumeric(it) || system.isScaleID(it)] +// // TODO also include expressions that contain two variables as its arguments +// // but this checking for conflicts is more difficult e.g. x < y, y < z, x < y +// args.length == 1 ? expressions.put(args.get(0), expr) +// } +// } +// ] +//// System.out.println('variable -> expression:\t' + expressions) +// +// // find possible values for each variable to make each expression either true or false +// // for numeric expressions x = 5, x < 3, x > 7 the values of x can be: 0, 5, 10 +// // for any boolean expression b: b will be 0 (false), 1 (true) +// // for any scale expression: the values will be the 0 .. #scaleParams - 1 +// val Multimap values = HashMultimap.create() +// expressions.asMap.forEach [ k, v | +// switch(k) { +// case system.isBoolean(k): +// values.get(k).addAll(0, 1) +// case system.isNumeric(k): { +// val getValue = [ RelComp expr | +// system.eval(expr.left) ?: system.eval(expr.right) +// ] +// val range = v.map(getValue).min - 1 .. v.map(getValue).max + 1 +// val Set> outcomes = new HashSet() +// values.putAll(k, range.filter [ i | +// val result = v.map [ expr | +// val left = system.eval(expr.left) ?: i +// val right = system.eval(expr.right) ?: i +// SLEECEvaluator.eval(left, expr.op, right) +// ].toList +// outcomes.add(result) +// ]) +// } +// case system.isScaleID(k): { +// val eval = [ MBoolExpr expr | +// switch (expr) { +// Atom: system.scales.get(k).indexOf(expr.measureID) +// } +// ] +// val range = 0 ..< system.scales.get(k).length +// val Set> outcomes = new HashSet() +// values.putAll(k, range.filter [ i | +// val result = v.map [ expr | +// val Integer left = eval.apply(expr.left) ?: i +// val Integer right = eval.apply(expr.right) ?: i +// SLEECEvaluator.eval(left, expr.op, right) +// ].toList +// outcomes.add(result) +// ]) +// } +// } +// ] +//// System.out.println('variable -> value:\t' + values) +// +// // map between a rule and the index of the index of the combination of values of variables if that combination triggered the rule +// // for: +// // Rule0 when Event0 and x = 5 or y = 3 then E1 +// // Rule1 when Event0 and x = 3 and y = 6 then E1 +// // values will be +// //{x = [x = 5, x = 3], y = [y = 3, y = 6]} +// // the cartesian product of the values will be: +// // {[x = 5, y = 3], [x = 5, y = 6], [x = 3, y = 3], [x = 3, y = 6]} +// // ruleeTriggered will be: +// // {Rule0 = [0, 1, 2], Rule1 = [3]} +// val Multimap ruleTriggered = HashMultimap.create() +// Sets.cartesianProduct(values.asMap.values.map[toSet]).forEach [ combination, i | +// val variables = (0 ..< combination.size).toMap([values.keySet.get(it)], [combination.get(it)]) +// val scales = new HashMap() +// system.scales.values.forEach [ +// forEach[k, v|scales.put(k, v)] +// ] +//// System.out.println(variables) +// val evaluator = new SLEECEvaluator(variables, system.constants, scales) +// ruleBlock.rules.forEach [ rule | +// evaluator.eval(rule) ? ruleTriggered.put(rule, i) +// ] +// ] +//// System.out.println('expressions:\t' + expressions.values.length + '\t' + expressions.values.join(' ')) +//// System.out.println('rule -> triggered?\t' + ruleTriggered) +// +// // group rules by matching trigger-response pair +// val Multimap, Rule> rules = HashMultimap.create() +// ruleBlock.rules.forEach [ rule | +// rules.put(rule.trigger.event.name -> rule.response.constraint.event.name, rule) +// ] +//// System.out.println('trigger -> response:\t' + rules) +// +// // check for conflicts and redundancies +// rules.asMap.forEach [ trigger, triggeredRules | +// for (i : 0 ..< triggeredRules.length){ +// +// val rule0 = triggeredRules.get(i) +// val set0 = ruleTriggered.get(rule0) +// +// for (j : i + 1 ..< triggeredRules.length) { +// +// val rule1 = triggeredRules.get(j) +// val set1 = ruleTriggered.get(rule1) +// // first check for conflicts +// // conflicts happen when responses in the form are both triggered at the same time +// // Event0 within x +// // not Event0 within y +// // where y < x +// if (rule0.response.constraint.not != rule1.response.constraint.not) { +// // only 1 of the 2 rules has a not in their response +// if (rule0.response.constraint.not && system.eval(rule0.response.constraint.value) < system.eval(rule1.response.constraint.value) || +// rule1.response.constraint.not && system.eval(rule0.response.constraint.value) > system.eval(rule1.response.constraint.value)) { +// error('''«rule0.name» conflicts with «rule1.name».''', rule0, SLEECPackage.Literals.RULE__NAME) +// error('''«rule1.name» conflicts with «rule0.name».''', rule1, SLEECPackage.Literals.RULE__NAME) +// return +// } +// +// } +// // then check for redundancies +// else { +// // either both rules have 'not' or don't have 'not' +// val rule0Redundant = set1.containsAll(set0) +// val rule1Redundant = set0.containsAll(set1) +// // rule0 is redundant if result == 1 +// // rule1 is redundant is result == -1 +// // no rules are redundant if result == 0 +// var result = +// if (rule0Redundant && (!rule1Redundant || system.eval(rule0.response.constraint.value) <= system.eval(rule1.response.constraint.value))) +// 1 +// else if (rule1Redundant) +// -1 +// // if both rules have not, invert the result +// rule0.response.constraint.not && rule1.response.constraint.not ? result = -result +// switch (result) { +// case 1: warning('''Redundant rule: «rule0.name», under «rule1.name».''', rule0, SLEECPackage.Literals.RULE__NAME) +// case -1: warning('''Redundant rule: «rule1.name», under «rule0.name».''', rule1, SLEECPackage.Literals.RULE__NAME) +// } +// } +// } +// } +// ] +// // Checks a rule's components are not self-conflicting // for (rule : ruleBlock.rules) {