Skip to content

GitLab

Commit 4d24eaa3 authored by Bruno Gomez's avatar Bruno Gomez
Browse files

remove unnecessary files. Automation of SpectraController synth. Fix to run... 

remove unnecessary files. Automation of SpectraController synth. Fix to run check LTL validations over SpectraController
parent d0b4df61
Pipeline #13709 failed with stages
in 19 minutes and 58 seconds
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 91 additions and 463 deletions
maven-root/mtsa/SpectraEngineResources/input/mtsa-automaton-trans.txt deleted 100644 → 0
View file @ d0b4df61
[States: [0, 1, 2, 3, 4, 5, 6]
Actions: [phil.0.arise, phil.0.eat, phil.0.left.put, phil.0.right.put, tau, phil.0.right.get, phil.0.left.get, phil.0.sitdown]
Required Transitions: {0=[(phil.0.sitdown,1)], 1=[(phil.0.right.get,2)], 2=[(phil.0.left.get,3)], 3=[(phil.0.eat,4)], 4=[(phil.0.left.put,5)], 5=[(phil.0.right.put,6)], 6=[(phil.0.arise,0)]}
Maybe Transitions: {0=[], 1=[], 2=[], 3=[], 4=[], 5=[], 6=[]}
, States: [0, 1]
Actions: [phil.1.right.put, phil.0.left.put, tau, phil.1.right.get, phil.0.left.get]
Required Transitions: {0=[(phil.1.right.get,1), (phil.0.left.get,1)], 1=[(phil.1.right.put,0), (phil.0.left.put,0)]}
Maybe Transitions: {0=[], 1=[]}
, States: [0, 1, 2, 3, 4, 5, 6]
Actions: [phil.1.right.put, phil.1.sitdown, tau, phil.1.left.get, phil.1.right.get, phil.1.eat, phil.1.arise, phil.1.left.put]
Required Transitions: {0=[(phil.1.sitdown,1)], 1=[(phil.1.right.get,2)], 2=[(phil.1.left.get,3)], 3=[(phil.1.eat,4)], 4=[(phil.1.left.put,5)], 5=[(phil.1.right.put,6)], 6=[(phil.1.arise,0)]}
Maybe Transitions: {0=[], 1=[], 2=[], 3=[], 4=[], 5=[], 6=[]}
, States: [0, 1]
Actions: [phil.0.right.put, tau, phil.1.left.get, phil.0.right.get, phil.1.left.put]
Required Transitions: {0=[(phil.1.left.get,1), (phil.0.right.get,1)], 1=[(phil.0.right.put,0), (phil.1.left.put,0)]}
Maybe Transitions: {0=[], 1=[]}
]
\ No newline at end of file
maven-root/mtsa/SpectraEngineResources/out/automata-old.lts deleted 100644 → 0
View file @ d0b4df61
S0 = (phil0sitdown -> S1 | phil1sitdown -> S1),
S1 = (phil0rightget -> S1 | phil1sitdown -> S2),
S2 = (phil0rightget -> S3 | phil1rightget -> S2),
S3 = (phil0leftget -> S4 | phil1rightget -> S3),
S4 = (phil0eat -> S5),
S5 = (phil0leftput -> S6),
S6 = (phil0rightput -> S6 | phil1rightget -> S7),
S7 = (phil0rightput -> S8),
S8 = (phil0arise -> S9 | phil1leftget -> S8),
S9 = (phil0sitdown -> S10 | phil1leftget -> S9),
S10 = (phil0rightget -> S10 | phil1leftget -> S11),
S11 = (phil1eat -> S12),
S12 = (phil1leftput -> S13),
S13 = (phil0rightget -> S0 | phil1rightput -> S13) + {phil1arise}.
maven-root/mtsa/SpectraEngineResources/out/automata.lts deleted 100644 → 0
View file @ d0b4df61
S0 = (phil0sitdown -> S1 | phil1sitdown -> S1),
S1 = (phil0rightget -> S1 | phil1sitdown -> S2),
S2 = (phil0rightget -> S2 | phil1rightget -> S3),
S3 = (phil0rightget -> S3 | phil1leftget -> S4),
S4 = (phil1eat -> S4) + {phil1arise, phil0eat, phil0arise, phil0rightput, phil1rightput, phil1leftput, phil0leftput, phil0leftget}.
maven-root/mtsa/src/main/java/MTSTools/ac/ic/doc/mtstools/model/operations/DCS/TranslateToRS/SpectraBDDParserIntegration.java
View file @ 4d24eaa3
......@@ -7,8 +7,6 @@ import java.io.*;
import java.nio.file.Path;
import java.nio.file.Paths;
import java.util.*;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
/**
* Clase de integración para el workflow MTSA → Spectra → Parser.
......@@ -23,7 +21,7 @@ public class SpectraBDDParserIntegration {
private static final String FSP_NAME = "C";
private final LTSOutput output;
private boolean debugMode = true;
private boolean debugMode = false;
public SpectraBDDParserIntegration(LTSOutput output) {
......@@ -50,9 +48,9 @@ public class SpectraBDDParserIntegration {
*/
public void synthesizeWithFullCLIParams(CompositeState compositeState, List<MTS<Long, String>> ltss, boolean enableMtsaGuide) throws Exception {
long startTime = System.currentTimeMillis();
long totalStart = System.currentTimeMillis();
// Resolve paths internally to avoid leaking config to callers
// Resolve paths
String inputBasePath = resolveInputBasePath();
String outputPath = resolveOutputPath();
String logPath = resolveLogPath(outputPath);
......@@ -60,31 +58,26 @@ public class SpectraBDDParserIntegration {
String parserJar = resolveParserJarPath(inputBasePath);
String actionVar = resolveActionVar();
// Paso 1: El .spectra ya fue generado por el caller (para evitar doble traducción).
// Step 1: .spectra already generated by caller
validateIfSpectraWasTranslated(inputBasePath);
output.outln("=== Step 1/3: MTSA to Spectra translated ===");
output.outln("[Step 1/3] MTSA -> Spectra: done (by caller)");
// Paso 2 y 3: Ejecutar parser con parámetros CLI completos
output.outln("\n=== Step 2/3: Preparing Spectra synthesis ===");
// Step 2: BDD synthesis via Spectra CLI
output.outln("\n[Step 2/3] BDD synthesis (Spectra CLI)...");
List<String> command = buildFullCLICommand(spectraCliJar, parserJar,
inputBasePath, outputPath, logPath,
enableMtsaGuide, actionVar, resolveNativeLibPath());
if (debugMode) {
output.outln("\nExecuting command:");
output.outln(String.join(" \\\n ", command));
output.outln(" Command: " + String.join(" \\\n ", command));
}
writeMtsAutomatonFile(inputBasePath, ltss);
long synthesisStart = System.currentTimeMillis();
StringBuilder parserOutput = new StringBuilder();
int exitCode = executeParser(command, parserOutput);
output.outln("=== Step 3/3: Parsing BDD to LTS ===");
long elapsed = System.currentTimeMillis() - startTime;
long synthesisElapsed = System.currentTimeMillis() - synthesisStart;
output.outln("\n=== Results ===");
output.outln("Total time: " + elapsed + " ms");
output.outln("Exit code: " + exitCode);
output.outln("[Step 2/3] BDD synthesis: " + synthesisElapsed + " ms (exit code: " + exitCode + ")");
if (exitCode != 0) {
output.outln("\n=== ERROR: Synthesis Failed ===");
......@@ -92,28 +85,31 @@ public class SpectraBDDParserIntegration {
throw new Exception("Spectra-BDD-Parser failed with exit code " + exitCode);
}
// Buscar y leer el archivo LTS generado
// Step 3: Parse generated LTS and build controller
output.outln("\n[Step 3/3] Parsing LTS and building controller...");
long parseStart = System.currentTimeMillis();
File ltsFile = findGeneratedLTSFile(new File(outputPath));
if (ltsFile != null && ltsFile.exists()) {
output.outln("\n=== Controller Generated ===");
output.outln("File: " + ltsFile.getName());
output.outln("Size: " + ltsFile.length() + " bytes");
FileInput lts = new FileInput(ltsFile);
LTSOutput output = new LTSOuputImpl();
LTSCompiler compiled = new LTSCompiler(lts, output, ".");
LTSOutput innerOutput = new LTSOuputImpl();
LTSCompiler compiled = new LTSCompiler(lts, innerOutput, ".");
compiled.compile();
Vector<CompactState> vector = new Vector<>();
CompositeState compositeStateC = compiled.continueCompilation(FSP_NAME);
compositeStateC.compose(output);
compositeStateC.compose(innerOutput);
vector.add(compositeStateC.getComposition());
compositeState.setMachines(vector);
compositeState.compose(output);
readFileContent(ltsFile);
//removeJitFilesGenerated(inputBasePath);
compositeState.compose(innerOutput);
removeFilesGenerated(inputBasePath);
long parseElapsed = System.currentTimeMillis() - parseStart;
long totalElapsed = System.currentTimeMillis() - totalStart;
output.outln("[Step 3/3] LTS parse + controller build: " + parseElapsed + " ms");
output.outln(" File: " + ltsFile.getName() + " (" + ltsFile.length() + " bytes)");
output.outln(" Total synthesis time: " + totalElapsed + " ms");
} else {
output.outln("\n=== WARNING: Controller file not found ===");
output.outln("Expected in: " + outputPath);
......@@ -127,7 +123,7 @@ public class SpectraBDDParserIntegration {
try (BufferedWriter writer = new BufferedWriter(new FileWriter(dest))) {
writer.write(ltss.toString());
}
output.outln("Written MTS oracle: " + dest.getAbsolutePath());
if(debugMode) output.outln("Written MTS oracle: " + dest.getAbsolutePath());
}
private int executeParser(List<String> command, StringBuilder parserOutput) throws IOException, InterruptedException {
......@@ -142,17 +138,16 @@ public class SpectraBDDParserIntegration {
String line;
while ((line = reader.readLine()) != null) {
parserOutput.append(line).append("\n");
if (debugMode) {
output.outln("[Parser] " + line);
}
if(debugMode) output.outln("[Parser] " + line);
}
}
int exitCode = process.waitFor();
return exitCode;
}
private void removeJitFilesGenerated(String inputBasePath) {
// Cleanup synthesized artifacts after adapter initialization
private void removeFilesGenerated(String inputBasePath) {
Path synthFiles = Paths.get(inputBasePath, "synth","jit","filename");
try (var walk = java.nio.file.Files.walk(synthFiles)) {
walk.sorted(java.util.Comparator.reverseOrder())
......@@ -164,6 +159,27 @@ public class SpectraBDDParserIntegration {
} catch (Exception ex) {
output.outln(String.format("Failed to clean synthesized files under %s: %s", synthFiles, ex.getMessage()));
}
if (debugMode) return;
File resourcesDir = new File(inputBasePath).getParentFile();
Path[] toDelete = {
Paths.get(inputBasePath, "filename.spectra"),
Paths.get(inputBasePath, "mtsa-automaton-trans.txt"),
Paths.get(resourcesDir.getPath(), "out", "automata.lts"),
Paths.get(resourcesDir.getPath(), "out", "log.txt")
};
for (Path p : toDelete) {
try {
if (java.nio.file.Files.deleteIfExists(p)) {
output.outln(" Deleted: " + p.getFileName());
}
} catch (Exception ex) {
output.outln(" Failed to delete " + p + ": " + ex.getMessage());
}
}
}
private String resolveActionVar() {
......
maven-root/mtsa/src/main/java/ltsa/dispatcher/TransitionSystemDispatcher.java
View file @ 4d24eaa3
......@@ -46,6 +46,7 @@ import ltsa.control.util.ControlConstants;
import ltsa.control.util.ControllerUtils;
import ltsa.lts.*;
import ltsa.lts.Minimiser;
import ltsa.lts.ltl.AssertDefinition;
import ltsa.lts.distribution.DistributionDefinition;
import ltsa.lts.distribution.DistributionTransformationException;
import ltsa.lts.util.MTSUtils;
......@@ -2977,25 +2978,27 @@ public class TransitionSystemDispatcher {
}
try {
// STEP 1: Generate Spectra file (single translation point)
output.outln("Generating Spectra specification...");
output.outln("\n=== Spectra-BDD-Parser Synthesis ===");
// STEP 1: Translate MTSA environment to Spectra
long translationStart = System.currentTimeMillis();
output.outln("[Step 1/3] Translating MTSA -> Spectra...");
TranslateToSpectra<Long, String> translator = new TranslateToSpectra<>();
translator.translate(ltss, goal.getControllableActions(),
new ArrayList<>(goal.getAssumptions()), new ArrayList<>(goal.getGuarantees()));
output.outln("[Step 1/3] Translation: " + (System.currentTimeMillis() - translationStart) + " ms");
// STEP 2: Run the parser with the generated file
output.outln("Starting BDD parser...");
SpectraBDDParserIntegration integration =
new SpectraBDDParserIntegration(output);
integration.synthesizeWithFullCLIParams(
compositeState,
ltss, true
);
// STEP 2+3: BDD parser (internally creates LTSCompiler which resets
// AssertDefinition's static definitions — save and restore around the call).
Object savedAssertState = AssertDefinition.saveState();
SpectraBDDParserIntegration integration = new SpectraBDDParserIntegration(output);
try {
integration.synthesizeWithFullCLIParams(compositeState, ltss, true);
} finally {
AssertDefinition.restoreState(savedAssertState);
}
output.outln("\n=== Synthesis Complete ===");
output.outln("Controller generated successfully");
} catch (Exception e) {
output.outln("\n=== ERROR: Synthesis Failed ===");
......
maven-root/mtsa/src/main/java/ltsa/lts/ltl/AssertDefinition.java
View file @ 4d24eaa3
......@@ -76,7 +76,19 @@ public class AssertDefinition {
definitions = null;
constraints = null;
}
public static Object saveState() {
return new Object[]{ definitions, constraints, PredicateDefinition.saveState() };
}
@SuppressWarnings("unchecked")
public static void restoreState(Object saved) {
Object[] arr = (Object[]) saved;
definitions = (Hashtable<String, AssertDefinition>) arr[0];
constraints = (Hashtable<String, AssertDefinition>) arr[1];
PredicateDefinition.restoreState(arr[2]);
}
public static String[] names() {
if (definitions==null) return null;
// int n = definitions.size();
......
maven-root/mtsa/src/main/java/ltsa/lts/ltl/PredicateDefinition.java
View file @ 4d24eaa3
......@@ -61,7 +61,16 @@ public class PredicateDefinition {
public static void init(){
definitions = null;
}
public static Object saveState() {
return definitions;
}
@SuppressWarnings("unchecked")
public static void restoreState(Object saved) {
definitions = (Hashtable) saved;
}
public static void compileAll() {
if (definitions == null) return;
List v = new ArrayList();
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment