From 5238c76c4ca3e78e08258480564c496606a1a5c1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 22 Jun 2015 18:41:05 +0000 Subject: [PATCH] Optimisation in the simulator for models with very large numbers of actions (from Marcus Daum + Joachim Klein). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10057 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/param/SymbolicEngine.java | 14 ++++++++++++-- prism/src/simulator/Updater.java | 8 +++++++- 2 files changed, 19 insertions(+), 3 deletions(-) diff --git a/prism/src/param/SymbolicEngine.java b/prism/src/param/SymbolicEngine.java index a2f14634..490b9e3f 100644 --- a/prism/src/param/SymbolicEngine.java +++ b/prism/src/param/SymbolicEngine.java @@ -29,6 +29,7 @@ package param; import java.util.ArrayList; import java.util.BitSet; +import java.util.HashSet; import java.util.List; import java.util.Vector; @@ -64,15 +65,24 @@ public class SymbolicEngine numModules = modulesFile.getNumModules(); synchs = modulesFile.getSynchs(); numSynchs = synchs.size(); + + // Compute count of number of modules using each synch action + // First, compute and cache the synch actions for each of the modules + List> synchsPerModule = new ArrayList>(numModules); + for (int i = 0; i < numModules; i++) { + synchsPerModule.add(new HashSet(modulesFile.getModule(i).getAllSynchs())); + } + // Second, do the counting synchModuleCounts = new int[numSynchs]; for (int j = 0; j < numSynchs; j++) { synchModuleCounts[j] = 0; String s = synchs.get(j); for (int i = 0; i < numModules; i++) { - if (modulesFile.getModule(i).usesSynch(s)) + if (synchsPerModule.get(i).contains(s)) synchModuleCounts[j]++; } - } + } + updateLists = new ArrayList>>(numModules); for (int i = 0; i < numModules; i++) { updateLists.add(new ArrayList>(numSynchs + 1)); diff --git a/prism/src/simulator/Updater.java b/prism/src/simulator/Updater.java index 6dcf11c2..f839330c 100644 --- a/prism/src/simulator/Updater.java +++ b/prism/src/simulator/Updater.java @@ -88,12 +88,18 @@ public class Updater extends PrismComponent this.varList = varList; // Compute count of number of modules using each synch action + // First, compute and cache the synch actions for each of the modules + List> synchsPerModule = new ArrayList>(numModules); + for (i = 0; i < numModules; i++) { + synchsPerModule.add(new HashSet(modulesFile.getModule(i).getAllSynchs())); + } + // Second, do the counting synchModuleCounts = new int[numSynchs]; for (j = 0; j < numSynchs; j++) { synchModuleCounts[j] = 0; s = synchs.get(j); for (i = 0; i < numModules; i++) { - if (modulesFile.getModule(i).usesSynch(s)) + if (synchsPerModule.get(i).contains(s)) synchModuleCounts[j]++; } }