Skip to content

Commit

Permalink
Merge commit 'c1ee09e4925ecd6c7220926fabc3581ba3183456' into main
Browse files Browse the repository at this point in the history
  • Loading branch information
pefribeiro committed Jun 18, 2024
2 parents f956f2a + c1ee09e commit 39fbaec
Show file tree
Hide file tree
Showing 5 changed files with 224 additions and 172 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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<? extends IOutputConfigurationProvider> bindIOutputConfigurationProvider() {
return SLEECOutputConfigurationProvider
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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 {

Expand Down Expand Up @@ -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
]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -58,22 +60,22 @@ class SLEECGenerator extends AbstractGenerator {

Set<String> scaleIDs
Set<String> 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}.
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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 = {||}
Expand Down Expand Up @@ -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»|}
Expand Down Expand Up @@ -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 = {|'''
Expand All @@ -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)

Expand Down Expand Up @@ -624,7 +630,8 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir
assertions+= '''-> MemoryInOrder
'''

assertions+= '''within
assertions+= '''
within
timed_priority(
(
(
Expand All @@ -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) |]
(
Expand All @@ -652,7 +662,7 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir
MemoryInOrder
)
) \MemoryInternalEvents
)
)
'''
}
}
Expand Down Expand Up @@ -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.
Expand All @@ -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 <pedro.ribeiro@york.ac.uk>
-- Department of Computer Science
-- University of York
Expand Down Expand Up @@ -1260,9 +1271,7 @@ assertions += '''assert not «secondRule.name»_wrt_«firstRule.name» [T= «fir

endmodule
---------------------------------------------------------------------------


'''
'''
)
}
Expand Down
Original file line number Diff line number Diff line change
@@ -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<OutputConfiguration>// 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

}
}
Loading

0 comments on commit 39fbaec

Please sign in to comment.