From 18d8ff15abeb2aecc3cdedb0eabb076b4b8f058c Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 29 Jul 2020 16:40:45 +0200 Subject: Fix time measurement --- .../.ApplicationConfigurationIdeModule.xtendbin | Bin 1701 -> 1701 bytes .../ide/.ApplicationConfigurationIdeSetup.xtendbin | Bin 2526 -> 2526 bytes .../.SolverSemanticHighlightCalculator.xtendbin | Bin 5334 -> 5334 bytes .../.SolverSemanticTextAttributeProvider.xtendbin | Bin 4902 -> 4902 bytes .../validation/.SolverLanguageValidator.xtendbin | Bin 1717 -> 1717 bytes ....SolverLanguageTokenDefInjectingParser.xtendbin | Bin 2742 -> 2742 bytes ...nguageSyntheticTokenSyntacticSequencer.xtendbin | Bin 2758 -> 2758 bytes .../rules/RefinementRuleProvider.xtend | 18 ++- .../viatra/dse/base/DesignSpaceManager.java | 2 +- .../case.study.familyTree.run/bin/.gitignore | 1 - .../config/genericFamilyTreeSMTQual.vsconfig | 3 + .../queries/SatelliteQueries.vql | 144 +-------------------- 12 files changed, 13 insertions(+), 155 deletions(-) delete mode 100644 Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin index 96d7f77b..2a740f24 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeModule.xtendbin differ diff --git a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin index 85768640..6fd0f505 100644 Binary files a/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin and b/Application/hu.bme.mit.inf.dslreasoner.application.ide/xtend-gen/hu/bme/mit/inf/dslreasoner/application/ide/.ApplicationConfigurationIdeSetup.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin index 287aa50d..0b252347 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticHighlightCalculator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin index e9b25b0a..930ba6bf 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/ui/syntaxcoloring/.SolverSemanticTextAttributeProvider.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin index 79d18e32..65fea578 100644 Binary files a/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin and b/Application/org.eclipse.viatra.solver.language.ui/xtend-gen/org/eclipse/viatra/solver/language/validation/.SolverLanguageValidator.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin index c529b829..340908fe 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/parser/antlr/.SolverLanguageTokenDefInjectingParser.xtendbin differ diff --git a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin index 9ff56ed9..21b52163 100644 Binary files a/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin and b/Application/org.eclipse.viatra.solver.language/xtend-gen/org/eclipse/viatra/solver/language/serializer/.SolverLanguageSyntheticTokenSyntacticSequencer.xtendbin differ diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend index f7fe97a3..699b095d 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/rules/RefinementRuleProvider.xtend @@ -372,19 +372,17 @@ class RefinementRuleProvider { val src = match.get(3) as DefinedElement val trg = match.get(4) as DefinedElement - queryEngine.delayUpdatePropagation [ - val startTime = System.nanoTime - createRelationLinkAction(src, trg, relationInterpretation) - statistics.addExecutionTime(System.nanoTime - startTime) - ] + val startTime = System.nanoTime + createRelationLinkAction(src, trg, relationInterpretation) + statistics.addExecutionTime(System.nanoTime - startTime) // Scope propagation if (scopePropagator.isPropagationNeededAfterAdditionToRelation(declaration)) { - queryEngine.delayUpdatePropagation [ - val propagatorStartTime = System.nanoTime - scopePropagator.propagateAllScopeConstraints() - statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) - ] + flushQueryEngine(scopePropagator) + + val propagatorStartTime = System.nanoTime + scopePropagator.propagateAllScopeConstraints() + statistics.addScopePropagationTime(System.nanoTime - propagatorStartTime) } ] } else { diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java index 7e7a6e51..133ef948 100644 --- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java +++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/base/DesignSpaceManager.java @@ -369,6 +369,7 @@ public class DesignSpaceManager implements IBacktrackListener { } catch (InvocationTargetException e) { throw new RuntimeException(e); } + backtrackingTime += System.nanoTime() - start; updateActivationCodes(); Object lastActivationId = trajectory.getLastActivationId(); @@ -382,7 +383,6 @@ public class DesignSpaceManager implements IBacktrackListener { } logger.debug("Backtrack."); - backtrackingTime += System.nanoTime() - start; return true; } diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore deleted file mode 100644 index 7050a7e3..00000000 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/bin/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/queries/ diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig index 80ab2906..fa9cd6e2 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig @@ -36,6 +36,9 @@ generate { log-level = normal, "fitness-punishSize" = "false", "fitness-scope" = "3", + "fitness-objectCreationCosts" = "true", + "scopePropagator" = "typeHierarchy", + "fitness-missing-containment" = "2", "numeric-solver-at-end" = "true" } diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql index 57b5933a..da889032 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/SatelliteQueries.vql @@ -245,146 +245,4 @@ pattern tooLowPathLengthForGroundStation(s:CommSubsystem) { GroundStationNetwork.commSubsystem(_,ts); check(l!=385000);//385.000km } -//// -//// Metrics -//// -// -//// Coverage -// -//pattern coverageMetric(Coverage : java Double) { -// Coverage == sum find missionCoverage(_, #_); -//} -// -//private pattern missionCoverage(Mission : InterferometryMission, Coverage : java Double) { -// InterferometryMission.observationTime(Mission, ObservationTime); -// ObserverCount == count find spacecraftWithInterferometryPayload(Mission, _); -// Coverage == eval(Math.pow(1 - 2.0 / ObserverCount, 1 + 9 * (1.0 / ObservationTime)) + 0.05 * ObservationTime / 3); -//} -// -//// Time -// -//pattern timeMetric(Time : java Double) { -// Time == sum find missionTime(_, #_); -//} -// -//private pattern missionTime(Mission : InterferometryMission, Time : java Double) { -// InterferometryMission.observationTime(Mission, ObservationTime); -// TrasmitTime == sum find transmitTime(Mission, _, #_); -// Time == eval(TrasmitTime + 60.0 * ObservationTime); -//} -// -//private pattern transmitTime(Mission : InterferometryMission, Spacecraft : Spacecraft, TransmitTime : java Double) { -// ConstellationMission.spacecraft(Mission, Spacecraft); -// find scienceData(Spacecraft, ScienceData); -// IncomingData == sum find incomingData(Spacecraft, _, #_); -// find transmitRate(Spacecraft, TransmitRate); -// TransmitTime == eval((ScienceData + IncomingData) / (7.5 * TransmitRate)); -//} -// -//private pattern incomingData(Spacecraft : Spacecraft, Source : Spacecraft, Data : java Double) { -// find indirectCommunicationLink(Source, Spacecraft); -// find scienceData(Source, Data); -//} -// -//private pattern scienceData(Spacecraft : Spacecraft, Data : java Double) { -// ConstellationMission.spacecraft(Mission, Spacecraft); -// InterferometryMission.observationTime(Mission, ObservationTime); -// Data == eval(12.0 * ObservationTime); -//} -// -//private pattern transmitRate(Spacecraft : Spacecraft, TransmitRate : java Double) { -// find spacecraftUplink(Spacecraft, Comm, Target); -// UHFCommSubsystem(Comm); -// Spacecraft(Target); -// TransmitRate == 5.0; -//} or { -// find spacecraftUplink(Spacecraft, Comm, Target); -// XCommSubsystem(Comm); -// Spacecraft(Target); -// TransmitRate == 1.6; -//} or { -// find spacecraftUplink(Spacecraft, Comm, Target); -// XCommSubsystem(Comm); -// GroundStationNetwork(Target); -// TransmitRate == 0.7; -//} or { -// find spacecraftUplink(Spacecraft, Comm, Target); -// KaCommSubsystem(Comm); -// Spacecraft(Target); -// TransmitRate == 220.0; -//} or { -// find spacecraftUplink(Spacecraft, Comm, Target); -// KaCommSubsystem(Comm); -// GroundStationNetwork(Target); -// TransmitRate == 80.0; -//} -// -//private pattern spacecraftUplink(Spacecraft : Spacecraft, TargetSubsystem : CommSubsystem, Target : CommunicatingElement) { -// CommunicatingElement.commSubsystem.target(Spacecraft, TargetSubsystem); -// CommunicatingElement.commSubsystem(Target, TargetSubsystem); -//} -// -//// Cost -// -//pattern costMetric(Cost : java Double) { -// Cost == sum find missionCost(_, #_); -//} -// -//private pattern missionCost(Mission : InterferometryMission, Cost : java Double) { -// InterferometryMission.observationTime(Mission, ObservationTime); -// SpacecraftCost == sum find spacecraftCost(Mission, _, #_); -// Cost == eval(SpacecraftCost + 100000.0 * ObservationTime); -//} -// -//private pattern spacecraftCost(Mission : InterferometryMission, Spacecraft : Spacecraft, Cost : java Double) { -// ConstellationMission.spacecraft(Mission, Spacecraft); -// find spacecraftOfKindCount(Spacecraft, KindCount); -// find basePrice(Spacecraft, BasePrice); -// find interferometryPayloadCost(Spacecraft, InterferometryPayloadCost); -// find additionalCommSubsystemCost(Spacecraft, AdditionalCommSubsystemCost); -// Cost == eval(BasePrice * Math.pow(KindCount, -0.25) + InterferometryPayloadCost + AdditionalCommSubsystemCost); -//} -// -//private pattern spacecraftOfKindCount(Sat : Spacecraft, Count : java Integer) { -// CubeSat3U(Sat); -// Count == count find cubeSat3U(_); -//} or { -// CubeSat6U(Sat); -// Count == count find cubeSat6U(_); -//} or { -// SmallSat(Sat); -// Count == count find smallSat(_); -//} -// -//private pattern basePrice(Spacecraft : Spacecraft, BasePrice : java Double) { -// CubeSat3U(Spacecraft); -// BasePrice == 250000.0; -//} or { -// CubeSat6U(Spacecraft); -// BasePrice == 750000.0; -//} or { -// SmallSat(Spacecraft); -// BasePrice == 3000000.0; -//} -// -//private pattern interferometryPayloadCost(Spacecraft : Spacecraft, Cost : java Double) { -// find spacecraftWithInterferometryPayload(_, Spacecraft); -// Cost == 50000.0; -//} or { -// neg find spacecraftWithInterferometryPayload(_, Spacecraft); -// Cost == 0.0; -//} -// -//private pattern additionalCommSubsystemCost(Spacecraft : Spacecraft, Cost : java Double) { -// find spacecraftWithTwoCommSubsystems(Spacecraft); -// Cost == 100000.0; -//} or { -// neg find spacecraftWithTwoCommSubsystems(Spacecraft); -// Cost == 0.0; -//} -// -//private pattern spacecraftWithTwoCommSubsystems(Spacecraft : Spacecraft) { -// Spacecraft.commSubsystem(Spacecraft, Subsystem1); -// Spacecraft.commSubsystem(Spacecraft, Subsystem2); -// Subsystem1 != Subsystem2; -//} + -- cgit v1.2.3-70-g09d2