FUNCTION no_cyclic_space_reference

(* SCHEMA step_merged_ap_schema; *)
-- IN AP242
FUNCTION no_cyclic_space_reference
      (spc : maths_space;
       refs : SET OF maths_space ) : BOOLEAN;
   LOCAL
      types : SET OF STRING;
      refs_plus : SET OF maths_space;
   END_LOCAL;
      IF spc IN refs THEN
         RETURN (FALSE);
      END_IF;
      types := TYPEOF(spc);
      refs_plus := refs + spc;
      IF schema_prefix + 'FINITE_SPACE' IN types THEN
         RETURN (bool(SIZEOF(QUERY (sp <* QUERY (mem <* spc\finite_space.members| (schema_prefix + 'MATHS_SPACE' IN TYPEOF(mem)))| NOT no_cyclic_space_reference(sp, refs_plus))) = 0));
      END_IF;
      IF schema_prefix + 'UNIFORM_PRODUCT_SPACE' IN types THEN
         RETURN (no_cyclic_space_reference(spc\uniform_product_space.base, refs_plus));
      END_IF;
      IF schema_prefix + 'LISTED_PRODUCT_SPACE' IN types THEN
         RETURN (bool(SIZEOF(QUERY (fac <* spc\listed_product_space.factors| NOT no_cyclic_space_reference(fac, refs_plus))) = 0));
      END_IF;
      IF schema_prefix + 'EXTENDED_TUPLE_SPACE' IN types THEN
         RETURN (no_cyclic_space_reference(spc\extended_tuple_space.base, refs_plus) AND no_cyclic_space_reference(spc\extended_tuple_space.extender, refs_plus));
      END_IF;
      RETURN (TRUE);
END_FUNCTION;

Referenced By

Defintion no_cyclic_space_reference is references by the following definitions:
DefinitionType
 extended_tuple_space ENTITY
 finite_space ENTITY
 listed_product_space ENTITY
 uniform_product_space ENTITY


[Top Level Definitions] [Exit]

Generated by STEP Tools® EXPRESS to HTML Converter
2017-01-19T11:17:24-05:00