Compute sizes based on FSM-representation

datatypes/subset_projection/GlobalTypeFSM.py

@@ -30,6 +30,8 @@ class GlobalTypeFSM:
         self.next_state_id = 0
         # generate a cache of subterms to states
         self.cache_subterm_state_list : list[(GlobalTypeParsed, State)] = []
+        # compute size on the fly
+        self.size = 0
         # generate the finite state machine and store the initial state
         self.initial_state = self.generate_FSM(globaltype)
 
@@ -47,10 +49,12 @@ class GlobalTypeFSM:
                 state_for_continuation = self.generate_FSM(continuation)
                 trans_state_list.append((msg_exchange, state_for_continuation))
             self.map_state_to_list_trans_state[state_for_subterm] = trans_state_list
+            self.size += len(trans_state_list)
         elif subterm.kind == GlobalTypeKinds.RECURSION:
             self.map_rec_var_to_state[subterm.bound_variable] = state_for_subterm
             state_for_continuation = self.generate_FSM(subterm.continuation)
             self.map_state_to_list_trans_state[state_for_subterm] = [(MessageExchangeEmpty(), state_for_continuation)]
+            self.size += 1
         elif subterm.kind == GlobalTypeKinds.REC_VAR:
             binder_state = self.map_rec_var_to_state.get(subterm.ref_variable)
             assert binder_state is not None
@@ -68,8 +72,12 @@ class GlobalTypeFSM:
         state_for_subterm = State(self.next_state_id)
         self.cache_subterm_state_list.append((subterm, state_for_subterm))
         self.next_state_id += 1
+        self.size += 1
         return state_for_subterm
 
+    def get_size(self):
+        return self.size
+
     def project_onto(self, proc) -> Optional[LocalFSM]:
         # 1) compute a projection by erasure onto the process so that the checks are faster later (not determinising)
         projection_by_erasure = ProjectionByErasure(self, proc)

datatypes/subset_projection/LocalFSM.py

@@ -25,12 +25,16 @@ class LocalFSM:
         return result
 
     def get_size(self):
+        size = 0
         visited = set()
         worklist = [self.initial_superstate]
         while len(worklist) > 0:
             to_expand = worklist.pop(0)
+            size += 1
             visited.add(to_expand)
-            for _, next_superstate in self.map_superstate_trans_superstate.get(to_expand, []):
+            list_of_transitions = self.map_superstate_trans_superstate.get(to_expand, [])
+            size += len(list_of_transitions)
+            for _, next_superstate in list_of_transitions:
                 if next_superstate not in visited:
                     worklist.append(next_superstate)
-        return len(visited)
\ No newline at end of file
+        return size
\ No newline at end of file

evaluation_functionality/EvalClassicalProjection.py

@@ -49,3 +49,7 @@ class EvalClassicalProjection:
     # calls the classical projection operator
     def project_onto(self, proc):
         return self.top_global_type.project_onto(proc)
+
+    # gives the size as global type
+    def get_size(self):
+        return self.top_global_type.get_size()

evaluation_functionality/evaluation_config.py

@@ -2,7 +2,7 @@ DEFAULT_NUM_RUNS = 10
 MAX_NUM_RUNS = 1000
 
 DEFAULT_MAX_SIZE_OVERHEAD = 250
-DEFAULT_MAX_SIZE_STATE_EXP = 100
+DEFAULT_MAX_SIZE_STATE_EXP = 175
 TIMEOUT_SCALE = 1000*60*10      # 10 minutes
 
 PREFIX_TYPES = "global_types/projectability/"

evaluation_functionality/run_evaluation.py

@@ -66,7 +66,7 @@ def run_projection_of_and_save_to(experiment_class, num_runs, example_name, path
            "\n"
     result_to_print = "yes" if expected_result else "no" # the expected_result is ensured to agree with the computed one
     average_time = sum_all / (float(num_runs))
-    res += "{:<7}".format("%3.0f" % gt.get_size()) + \
+    res += "{:<7}".format("%3.0f" % eval_object.get_size()) + \
            "{:<7}".format("%0.3f" % average_time) + \
             "{:<7}".format("%3.0f" % num_procs) + \
             "{:<14}".format("%3.0f" % size_projs) + \

evaluation_functionality/run_evaluation_state_explosion.py

@@ -30,7 +30,7 @@ def run_state_space_explosion_analysis(num_size):
         # we switch the validity check conditions off for this experiment
         # yielding subset constructions of the same size as subset projections
         os.environ['VALIDITY_CHECK'] = "FALSE"
-        compute_subset_constrution_up_to_size(example, spec_eval_folder_path, num_size, True)
+        compute_subset_construction_up_to_size(example, spec_eval_folder_path, num_size)
         os.environ['VALIDITY_CHECK'] = "TRUE"
         # c) create mappings
         # write_param_file_to_file(spec_eval_folder_path, example)
@@ -44,7 +44,7 @@ def write_global_types_up_to_size(whichone, size, snd=None):
     ParametricGlobalTypes.write_representation_up_to_size_w_kind(whichone, size, snd)
 
 
-def compute_subset_constrution_up_to_size(whichone, eval_path, num_size, check_avail=True, snd=None, prefix=''):
+def compute_subset_construction_up_to_size(whichone, eval_path, num_size):
     increase_rec_depth_and_RAM(ram=1000*1024*1024, rec_limit=10000)
     kind = whichone
     max_size = num_size
@@ -61,7 +61,8 @@ def compute_subset_constrution_up_to_size(whichone, eval_path, num_size, check_a
     i = start
     filename = filename_prefix + str(i) + ".gt"
     gt = get_gt_from_file(filename)
-    while gt.get_size() <= max_size:
+    fsm = GlobalTypeFSM(gt)
+    while fsm.get_size() <= max_size:
         filename = filename_prefix + str(i) + ".gt"
         gt = get_gt_from_file(filename)
         fsm = GlobalTypeFSM(gt)
@@ -73,11 +74,11 @@ def compute_subset_constrution_up_to_size(whichone, eval_path, num_size, check_a
         end = time.time()
         this_time_overall = 1000 * (end-start)
         size_all = size_projs["P"] + size_projs["Q"] + size_projs["R"]
-        res = "{:8}".format(str(gt.get_size())) + \
+        res = "{:8}".format(str(fsm.get_size())) + \
               "{:8}".format(str(i)) + \
-              "{:35}".format(str(size_projs["P"])) + \
-              "{:35}".format(str(size_projs["Q"])) + \
-              "{:35}".format(str(size_projs["R"])) + \
+              "{:35}".format(str(size_projs.get("P"))) + \
+              "{:35}".format(str(size_projs.get("Q"))) + \
+              "{:35}".format(str(size_projs.get("R"))) + \
               "{:35}".format(str(size_all)) + '\n'
         text_file.write(res)
         text_file.flush()