SheafSystem  0.0.0.0
poset_state_handle.cc
Go to the documentation of this file.
1 
2 //
3 // Copyright (c) 2014 Limit Point Systems, Inc.
4 //
5 // Licensed under the Apache License, Version 2.0 (the "License");
6 // you may not use this file except in compliance with the License.
7 // You may obtain a copy of the License at
8 //
9 // http://www.apache.org/licenses/LICENSE-2.0
10 //
11 // Unless required by applicable law or agreed to in writing, software
12 // distributed under the License is distributed on an "AS IS" BASIS,
13 // WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
14 // See the License for the specific language governing permissions and
15 // limitations under the License.
16 //
17 
20 
21 #include "SheafSystem/poset_state_handle.h"
22 
23 #include "SheafSystem/array_index_space_state.h"
24 #include "SheafSystem/array_poset_dof_map.h"
25 #include "SheafSystem/factory.h"
26 #include "SheafSystem/index_equivalence_iterator.h"
27 #include "SheafSystem/index_space_interval.h"
28 #include "SheafSystem/explicit_index_space_state.h"
29 #include "SheafSystem/implicit_crg_interval.h"
30 class index_iterator;
31 #include "SheafSystem/index_space_iterator.h"
32 #include "SheafSystem/namespace_poset.impl.h"
33 #include "SheafSystem/namespace_poset_member.h"
34 #include "SheafSystem/poset_bounds.h"
35 #include "SheafSystem/poset_crg_state.h"
36 #include "SheafSystem/poset_dof_map.h"
37 #include "SheafSystem/poset_handle_factory.h"
38 #include "SheafSystem/poset_member.h"
39 #include "SheafSystem/poset_member_iterator.h"
40 #include "SheafSystem/poset_dof_iterator.h"
41 #include "SheafSystem/poset_orderer.h"
42 #include "SheafSystem/poset_powerset_state.h"
43 #include "SheafSystem/poset_slicer.h"
44 #include "SheafSystem/poset_type.h"
45 #include "SheafSystem/postorder_member_iterator.h"
46 #include "SheafSystem/preorder_member_iterator.h"
47 #include "SheafSystem/primitives_poset.h"
48 #include "SheafSystem/primitives_poset_schema.h"
49 #include "SheafSystem/schema_poset_member.h"
50 #include "SheafSystem/assert_contract.h"
51 #include "SheafSystem/std_cstdlib.h"
52 #include "SheafSystem/std_iomanip.h"
53 #include "SheafSystem/std_sstream.h"
54 #include "SheafSystem/std_sstream.h"
55 #include "SheafSystem/subposet.h"
56 #include "SheafSystem/subposet_state.h"
57 #include "SheafSystem/subposet_member_iterator.h"
58 #include "SheafSystem/zn_to_bool.h"
59 
60 using namespace std;
61 
62 // ===========================================================
63 // POSET_STATE_HANDLE FACET
64 // ===========================================================
65 
66 // PUBLIC FUNCTIONS
67 
68 
71 new_poset_handle(const std::string& xclass_name,
72  poset_type xsheaf_base_class_id)
73 {
74  poset_state_handle* result;
75 
76  // Preconditions:
77 
78  // Body:
79 
80  result = factory().new_poset_handle(xclass_name, xsheaf_base_class_id);
81 
82  // Postconditions:
83 
84  ensure(result != 0);
85  ensure(!result->is_attached());
86 
87  // Exit:
88 
89  return result;
90 }
91 
92 // PROTECTED FUNCTIONS
93 
97 {
98  // Preconditions:
99 
100  // Body:
101 
102  static poset_handle_factory result;
103 
104  // Postconditions:
105 
106  // Exit:
107 
108  return result;
109 }
110 
113 {
114  _name_space = 0;
115  _state = 0;
116  _top = new total_poset_member;
117  _bottom = new total_poset_member;
118 
119 }
120 
123 {
124  // Preconditions:
125 
126  require(!is_attached());
127 
128  // Body:
129 
130  delete _top;
131  delete _bottom;
132 
133  // Postconditions:
134 
135  // Exit
136 
137  return;
138 }
139 
142 {
143  // Preconditions:
144 
145  require(xtop != 0);
146  require(!xtop->is_attached());
147  require(xbottom != 0);
148  require(!xbottom->is_attached());
149 
150  // Body:
151 
152  _name_space = 0;
153  _state = 0;
154  _top = xtop;
155  _bottom = xbottom;
156 
157  // Postconditions:
158 
159  ensure(!is_attached());
160  ensure(&(top()) == xtop);
161  ensure(&(bottom()) == xbottom);
162  ensure(!top().is_attached());
163  ensure(!bottom().is_attached());
164 
165  // Exit
166 
167  return;
168 }
169 
170 // PRIVATE FUNCTIONS
171 
172 
173 // ===========================================================
174 // STATE FACET
175 // ===========================================================
176 
177 // PUBLIC FUNCTIONS
178 
181 type_id() const
182 {
183  poset_type result;
184 
185  // Preconditions:
186 
187  require(state_is_read_accessible());
188 
189  // Body:
190 
191  result = state_obj()->type_id();
192 
193  // Postconditions:
194 
195  // Exit
196 
197  return result;
198 }
199 
200 const char*
202 class_name() const
203 {
204  // Preconditions:
205 
206  // Body:
207 
208  static const char* result = "poset_state_handle";
209 
210  // Postconditions:
211 
212  // Exit:
213 
214  return result;
215 }
216 
217 bool
219 is_external() const
220 {
221  bool result;
222 
223  // Preconditions:
224 
225  // Body:
226 
227  result = !is_attached() &&
228  (name_space() != 0) &&
229  (index().is_valid());
230 
231  // Postconditions:
232 
233  ensure(result ? !is_attached() : true);
234  ensure(result ? name_space() != 0 : true);
235  ensure(result ? index().is_valid() : true);
236 
237  // Exit
238 
239  return result;
240 }
241 
242 void
244 begin_jim_edit_mode(bool xauto_access)
245 {
246  // Preconditions:
247 
248  require(!xauto_access ? state_is_read_write_accessible() : true);
249 
250  // Body:
251 
252  if(xauto_access)
253  {
254  get_read_write_access(true);
255 
256  // Matching release access is in end_jim_edit_mode.
257  }
258 
259  define_old_variable(int old_jim_edit_depth = crg().jim_edit_depth());
260 
261  crg().request_jim_edit_mode();
262 
263  // Postconditions:
264 
265  ensure(state_is_read_write_accessible());
266  ensure(in_jim_edit_mode());
267  ensure(jim_edit_depth(false) == old_jim_edit_depth + 1);
268 
269  // Exit
270 
271  return;
272 }
273 
274 void
276 end_jim_edit_mode(bool xensure_lattice_invariant,
277  bool xauto_access)
278 {
279  // Preconditions:
280 
281  require(in_jim_edit_mode());
282  require(state_is_read_write_accessible());
283 
284  // Body:
285 
286  define_old_variable(int old_jim_edit_depth = crg().jim_edit_depth());
287 
288  crg().release_jim_edit_mode();
289 
290  // If we've fully released jim edit mode and the client requested it,
291  // re-establish the order relation and lattice invariants
292 
296 
297  if(xensure_lattice_invariant && !crg().jim_edit_mode())
298  {
299  ensure_lattice_invariant();
300  }
301 
302  if(xauto_access)
303  {
304  // Matching get access is in begin_jim_edit_mode().
305 
306  release_access();
307  }
308 
309  // Postconditions:
310 
311  ensure(jim_edit_depth(xauto_access) == old_jim_edit_depth - 1);
312 
313  // Exit
314 
315  return;
316 }
317 
318 bool
321 {
322  bool result;
323 
324  // Preconditions:
325 
326  // Body:
327 
328  result = state_is_read_write_accessible() && crg().jim_edit_mode();
329 
330  // Postconditions:
331 
332  ensure(result ? state_is_read_write_accessible() : true);
333 
334  // Exit:
335 
336  return result;
337 }
338 
339 int
341 jim_edit_depth(bool xauto_access) const
342 {
343  int result;
344 
345  // Preconditions:
346 
347  require(xauto_access || state_is_read_accessible());
348 
349  // Body:
350 
351  if(xauto_access)
352  {
353  get_read_access();
354  }
355 
356  result = crg().jim_edit_depth();
357 
358  if(xauto_access)
359  {
360  release_access();
361  }
362 
363  // Postconditions:
364 
365  ensure(result >= 0);
366 
367  // Exit:
368 
369  return result;
370 }
371 
372 void
375 {
376  // Preconditions:
377 
378  require(is_attached());
379 
380  // Body:
381 
382  int old_access_request_depth = access_request_depth();
383 
384  read_write_monitor_handle::get_read_access();
385  schema().get_read_access();
386 
387  // Postconditions:
388 
389  ensure(state_is_read_accessible());
390  ensure(access_request_depth() > old_access_request_depth);
391 
392  // Exit
393 
394  return;
395 }
396 
397 void
399 get_read_write_access(bool xrelease_read_only_access)
400 {
401  // Preconditions:
402 
403  require(is_attached());
404  require(!xrelease_read_only_access ? state_is_not_read_only_accessible() : true);
405 
406  // Body:
407 
408  int old_access_request_depth = access_request_depth();
409 
410  read_write_monitor_handle::get_read_write_access(xrelease_read_only_access);
411  schema().get_read_access();
412 
413  // Postconditions:
414 
415  ensure(state_is_read_write_accessible());
416  ensure(access_request_depth() > old_access_request_depth);
417 
418  // Exit
419 
420  return;
421 }
422 
423 void
425 release_access(bool xall) const
426 {
427  // Preconditions:
428 
429  require(state_is_read_accessible());
430 
431  // Body:
432 
433  int old_access_request_depth = access_request_depth();
434 
435  // Release at least one level of access for this..
436  // If xall, release all levels of access for this.
437  // Since each level of access to this also
438  // acquired a level of access to the schema,
439  // release the same number of levels of access to the schema.
440  // Note that this may not be all the levels of access of the schema.
441 
442  do
443  {
444  // Release one level of access.
445 
446  schema().release_access(false);
447  read_write_monitor_handle::release_access(false);
448  }
449  while(xall && state_is_read_accessible());
450 
451 
452  // Postconditions:
453 
454  ensure(xall ?
455  access_request_depth() == 0 :
456  access_request_depth() < old_access_request_depth);
457  ensure(access_request_depth() == 0 ? state_is_not_read_accessible() : true);
458 
459  // Exit
460 
461  return;
462 }
463 
464 bool
466 is_attached() const
467 {
468  bool result;
469 
470  // Preconditions:
471 
472  // Body:
473 
476 
477  result = (state_obj() != 0);
478 
479  // Postconditions:
480 
481  // Exit
482 
483  return result;
484 }
485 
486 bool
488 is_same_state(const poset_state_handle* xother) const
489 {
490  bool result;
491 
492  // Preconditions:
493 
494  // Body:
495 
496  result = (state_obj() == xother->state_obj());
497 
498  // Postconditions:
499 
500  // Exit
501 
502  return result;
503 }
504 
505 // PROTECTED FUNCTIONS
506 
509 state_obj() const
510 {
511  poset_state* result;
512 
513  // Preconditions:
514 
515  // Body:
516 
517  result = _state;
518 
519  // Postconditions:
520 
521  // Exit
522 
523  return result;
524 }
525 
526 void
529 {
530  // Preconditions:
531 
532  require(xother != 0);
533  require(xother->state_is_read_accessible());
534 
538 
539  // Body:
540 
541  _name_space = xother->name_space();
542  _index = xother->index();
543  _state = xother->state_obj();
544 
545  attach_handle_data_members();
546 
547  // Postconditions:
548 
549  ensure(poset_state_handle::invariant());
550  ensure(is_attached());
551  ensure(host() == xother->host());
552  ensure(index() == xother->index());
553 
554  return;
555 }
556 
557 
558 void
561 {
562  // Preconditions:
563 
564  require(xhost != 0);
565  require(xhost->state_is_read_accessible());
566  require(xhost->contains_member(xindex, false));
567 
568  // Body:
569 
570  // Create a handle to the xindex member of the namespace
571 
572  total_poset_member mbr(xhost, xindex);
573 
574  attach_to_state(&mbr);
575 
576  // We're finished with member,
577  // detach it so the state won't be deleted.
578 
579  mbr.detach_from_state();
580 
581  // Postconditions:
582 
583  ensure(postcondition_of(poset_state_handle::attach_to_state(abstract_poset_member*)));
584 
585  return;
586 }
587 
588 void
590 attach_to_state(const namespace_poset* xhost, const scoped_index& xindex)
591 {
592  // Preconditions:
593 
594  require(xhost != 0);
595  require(xhost->state_is_read_accessible());
596  require(xhost->contains_member(xindex, false));
597 
598  // Body:
599 
600  attach_to_state(xhost, xindex.hub_pod());
601 
602  // Postconditions:
603 
604  ensure(postcondition_of(poset_state_handle::attach_to_state(abstract_poset_member*)));
605 
606  return;
607 }
608 
609 void
611 attach_to_state(const namespace_poset* xhost, const std::string& xname)
612 {
613  // Preconditions:
614 
615  require(xhost != 0);
616  require(xhost->state_is_read_accessible());
617  require(xhost->contains_member(xname, false));
619 
620  // Body:
621 
622  // Create a handle to the xindex member of the namespace
623 
624  namespace_poset_member mbr(xhost, xname);
625 
626  attach_to_state(&mbr);
627 
628  // We're finished with member,
629  // detach it so the state won't be deleted.
630 
631  mbr.detach_from_state();
632 
633  // Postconditions:
634 
635  ensure(postcondition_of(poset_state_handle::attach_to_state(abstract_poset_member*)));
636 
637  return;
638 }
639 
640 void
643 {
644  // Preconditions:
645 
647 
648  require(xmbr != 0);
649  require(dynamic_cast<namespace_poset*>(xmbr->host()) != 0);
650  require(xmbr->state_is_read_accessible());
651  require(xmbr->is_jim());
653  require(unexecutable(xmbr->poset_pointer() == 0 ? xmbr->state_is_read_write_accessible() : true));
654 
655 
656  // Body:
657 
658  _name_space = dynamic_cast<namespace_poset*>(xmbr->host());
659  _index = xmbr->index();
660 
661  // $$CONST need to try and remove the const_cast here. The dynamic_cast stays.
662  namespace_poset_dof_map& ldof_map = dynamic_cast<namespace_poset_dof_map&>(const_cast<abstract_poset_member*>(xmbr)->dof_map(false));
663  poset_state_handle* handle_ptr = ldof_map.poset_pointer();
664 
665  if(handle_ptr != 0)
666  {
667  // Make this a handle for the same state; may be external.
668 
669  _state = handle_ptr->state_obj();
670  }
671  else
672  {
673  // Make this a handle for an external state;
674  // requires write access to dof tuple.
675 
676  _state = 0;
677  ldof_map.put_poset_pointer(this);
678  // ldof_map.put_poset_type_id(type_id());
681  }
682 
683  int old_access_request_depth = 0;
684  if(is_attached())
685  {
686  // State is not external; initialize the
687  // handle data members to values from the state.
688  // Requires read access.
689 
690  old_access_request_depth = access_request_depth();
691  poset_state_handle::get_read_access();
692 
693  attach_handle_data_members();
694  }
695 
696  // Postconditions:
697 
698  ensure(poset_state_handle::invariant());
699  ensure(host() == xmbr->host());
700  ensure(index() == xmbr->index());
701  ensure(!is_external() ? is_attached() : true);
702 
703  // Release access to poset state.
704 
705  if(is_attached()) poset_state_handle::release_access();
706 
707  // Ensure we left it in the access state we found it in.
708 
709  ensure(is_attached() ? access_request_depth() == old_access_request_depth : true);
710 
711  return;
712 }
713 
714 void
717 {
718 
719  // Preconditions:
720 
721  // Body:
722 
723  // Detach standard subposets.
724 
725  resident().detach_from_state();
726 
727  // Detach standard members.
728 
729  top().detach_from_state();
730  bottom().detach_from_state();
731 
732  // Detach from the name space.
733 
734  _name_space = 0;
735  _index.invalidate();
736 
737  // Detach from the state itself.
738 
739  _state = 0;
740 
741  // Postconditions:
742 
743  ensure(!is_attached());
744  ensure(!is_external());
745 
746  // Exit
747 
748  return;
749 }
750 
751 // void
752 // sheaf::poset_state_handle::
753 // delete_state(bool xauto_access)
754 // {
755 
756 // // Preconditions:
757 
758 // require(is_attached());
759 // require(xauto_access || state_is_read_write_accessible());
760 // require(xauto_access || (name_space() == 0) || name_space()->in_jim_edit_mode());
761 
762 // // Body:
763 
764 // namespace_poset* lns = name_space();
765 
766 // if(xauto_access)
767 // {
768 // get_read_write_access(true);
769 // }
770 
771 // // Detach from and delete the state.
772 
773 // scoped_index lindex = _index;
774 // terminate_access();
775 
776 // if(lns != 0)
777 // {
778 // // This is in a namespace; get access to it.
779 
780 // if(xauto_access)
781 // {
782 // lns->begin_jim_edit_mode(true);
783 // }
784 
785 // // Detach the handle held by the namespace member;
786 // // may be this, but another detach won't hurt.
787 
788 // lns->member_poset(lindex, false)->detach_from_state();
789 
790 // // Clean up the member dof tuple.
791 
792 // namespace_poset_member lns_mbr(lns, lindex);
793 // lns_mbr.put_poset_pointer(0);
794 // lns_mbr.put_poset_type_id(NOT_A_POSET_TYPE);
795 // lns_mbr.put_poset_class("");
796 
797 // // Delete the member.
798 
799 // lns_mbr.delete_state(false);
800 
801 // if(xauto_access)
802 // {
803 // lns->end_jim_edit_mode(true, true);
804 // }
805 // }
806 
807 // // Postconditions:
808 
809 // ensure(!is_attached());
810 
811 // // Exit
812 
813 // return;
814 // }
815 
816 void
818 new_state(namespace_poset& xns, const poset_path& xpath, const schema_poset_member& xschema, array_poset_dof_map& xdof_map)
819 {
820  // cout << endl << "Entering poset_state_handle::new_state." << endl;
821 
822  // Preconditions:
823 
824  require(!xpath.empty());
825  require(!xns.contains_poset(xpath, true));
826 
827  require(schema_is_ancestor_of(&xschema));
828  require(xschema.state_is_read_accessible());
829  require(xschema.host()->name_space()->is_same_state(&xns));
830 
831  // Body:
832 
833  // Create the state.
834 
835  new_state(xpath, xschema, xdof_map);
836 
837  // Insert it in the namespace.
838 
839  initialize_namespace(xns, xpath.poset_name(), true);
840 
841  // Postconditions:
842 
843  ensure(is_attached());
844  ensure(path(true).poset_name() == xpath.poset_name());
845  ensure(schema(true).is_same_state(&xschema));
846 
847  get_read_access();
848  ensure(&table_dof_map(false) == &xdof_map);
849  release_access();
850 
851 
852  // Exit:
853 
854  // cout << "Leaving poset_state_handle::new_state." << endl;
855  return;
856 }
857 
858 
859 void
861 new_state(const poset_path& xpath, const schema_poset_member& xschema, array_poset_dof_map& xdof_map)
862 {
863  // cout << endl << "Entering poset_state_handle::new_state." << endl;
864 
865  // Preconditions:
866 
867  require(!xpath.empty());
868  require(!xpath.full());
869 
870  require(schema_is_ancestor_of(&xschema));
871  require(xschema.state_is_read_accessible());
872 
875 
877 
878  require(unexecutable(xschema.is_same_state(xdof_map.schema())));
879 
880  // Body:
881 
882  is_abstract();
883 
884  // Postconditions:
885 
886  ensure(invariant());
887  ensure(is_attached());
888  ensure(!in_jim_edit_mode());
889  ensure(schema().is_same_state(&xschema));
890  ensure(has_standard_member_ct());
891  ensure(has_standard_row_dof_tuple_ct());
892  ensure(version() == COARSEST_COMMON_REFINEMENT_VERSION);
893 
894  // Now we're finished, release all access
895 
896  release_access();
897 
898  // One final postcondition
899 
900  ensure(state_is_not_read_accessible());
901 
902  // Exit:
903 
904  // cout << "Leaving poset_state_handle::new_state." << endl;
905  return;
906 }
907 
908 void
911 {
912  // Preconditions:
913 
914  require(state_is_read_accessible());
915  require(unexecutable("table dof tuple is valid"));
916 
917  // Body:
918 
919  // Initialize and attach those handle data members that
920  // are required by the access control routines; especially
921  // those that depend on the table dofs.
922 
923  // Does nothing in the class;
924  // intended to be redefined in descendants.
925 
926  // Postconditions:
927 
928 
929  // Exit
930 
931  return;
932 }
933 
934 void
937 {
938  // Preconditions:
939 
940  require(state_is_read_accessible());
941 
942  // Body:
943 
947 
948  disable_invariant_check();
949 
950  // Attach the handles for the standard subposets
951 
952  resident().attach_to_state(this, RESIDENT_INDEX);
953 
954  // Attach the handles for the standard members
955 
956  bottom().attach_to_state(this, BOTTOM_INDEX);
957  top().attach_to_state(this, TOP_INDEX);
958 
959  enable_invariant_check();
960 
961  // Postconditions:
962 
963  ensure(bottom().is_attached());
964  ensure(top().is_attached());
965  ensure(jims().is_attached());
966  ensure(whole().is_attached());
967  ensure(resident().is_attached());
968 
969  // Exit
970 
971  return;
972 }
973 
974 void
977 {
978 
979  // Preconditions:
980 
981  // Body:
982 
983  // Ensure for all members m: bottom <= m <= top.
984 
985  // Get an iterator for all the members.
986 
987  index_iterator itr = whole().indexed_member_iterator();
988 
989  // Skip by the bottom and top.
991 
992  itr.next();
993  itr.next();
994 
995  if(!itr.is_done())
996  {
997  // The poset is not empty (contains more than just top and bottom).
998  // We'll need the least join equivalement member of the top
999  // and the greatest join equivalent member of the bottom.
1000 
1001  pod_index_type least_top_jem = least_jem(TOP_INDEX);
1002  pod_index_type greatest_bottom_jem = greatest_jem(BOTTOM_INDEX);
1003 
1004  // Find all unlinked members and link them up.
1005 
1008 
1009  while(!itr.is_done())
1010  {
1011  pod_index_type lindex = itr.index().hub_pod();
1012 
1013  if(cover_is_empty(UPPER, lindex))
1014  {
1015  // Member is topless, link to to top.
1016 
1017  new_link(TOP_INDEX, lindex);
1018  }
1019 
1020  if(cover_is_empty(LOWER, lindex))
1021  {
1022  // Member is bottomless, link it to
1023  // least_bottom_jem
1024 
1027 
1028  new_link(lindex, greatest_bottom_jem);
1029  }
1030  itr.next();
1031  }
1032 
1033  // Ensure the order relation.
1034 
1035  poset_orderer orderer(this);
1036  orderer.restore_order();
1037  }
1038 
1039  // Postconditions:
1040 
1041  ensure( top().is_attached() );
1042  ensure(unexecutable(only top has no upper cover));
1043  ensure(unexecutable(order relation is well defined));
1044 
1045  // Exit
1046 
1047  return;
1048 }
1049 
1050 void
1053 {
1054  // Preconditions:
1055 
1056  require(state_is_read_write_accessible());
1057 
1058  // Body:
1059 
1060  define_old_variable(int old_schema_access_request_depth = schema().access_request_depth());
1061  int old_access_request_depth = access_request_depth();
1062 
1063 #ifdef DIAGNOSTIC_OUTPUT
1064  cout << "poset: " << name()
1065  << " old level:" << old_access_request_depth
1066  << " schema: " << schema().name();
1067 #endif
1068 
1069 
1070  // Release all levels of access this poset has to its schema,
1071  // but do not release access to the state of this because
1072  // we are going to delete the state and don't want another
1073  // client able to sneak in and get access before we do.
1074 
1078 
1079  for(size_type i=0; i<old_access_request_depth; ++i)
1080  {
1081  schema().release_access(false);
1082  }
1083 
1084  define_old_variable(int schema_access_request_depth = schema().access_request_depth());
1085 
1086 #ifdef DIAGNOSTIC_OUTPUT
1087  cout << " old level:" << old_schema_access_request_depth
1088  << " level: " << schema_access_request_depth
1089  << endl;
1090 #endif
1091 
1092  // Detach and delete the state.
1093 
1094  poset_state* lstate = _state;
1095  detach_from_state();
1096  delete lstate;
1097 
1098  // Postconditions:
1099 
1100  ensure(!is_attached());
1101  ensure(unexecutable("state has been deleted"));
1102  ensure(schema_access_request_depth == (old_schema_access_request_depth - old_access_request_depth));
1103 
1104  // Exit
1105 
1106  return;
1107 }
1108 
1109 // PRIVATE FUNCTIONS
1110 
1111 
1112 // ===========================================================
1113 // GLOBAL ATTRIBUTES FACET
1114 // ===========================================================
1115 
1116 // PUBLIC FUNCTIONS
1117 
1120 host() const
1121 {
1122  return name_space();
1123 }
1124 
1127 name_space() const
1128 {
1129  return _name_space;
1130 }
1131 
1132 const sheaf::scoped_index&
1134 index() const
1135 {
1136  // Preconditions:
1137 
1138  // Body:
1139 
1140  define_old_variable(const scoped_index& result = _index);
1141 
1142  // Postconditions:
1143 
1144  ensure(result.is_hub_scope() || !result.is_valid());
1145  ensure(result.is_positive() || !result.is_valid());
1146 
1147  // Exit
1148 
1149  return _index;
1150 }
1151 
1154 primitives() const
1155 {
1156 
1157  // Preconditions:
1158 
1159  require(state_is_read_accessible());
1160 
1161  // Body:
1162 
1163  primitives_poset& result = host()->primitives();
1164 
1165  // Postconditions:
1166 
1167  // Exit
1168 
1169  return result;
1170 }
1171 
1172 std::string
1174 name() const
1175 {
1176  string result;
1177 
1178  // Preconditions:
1179 
1180  require(is_external() ? name_space()->state_is_read_accessible() : state_is_read_accessible());
1181 
1182  // Body:
1183 
1184  if(is_external())
1185  {
1186  // Poset has no state yet, but nme is
1187  // same as name of associated member in name space.
1188 
1189  result = name_space()->member_name(index(), false);
1190  }
1191  else
1192  {
1193  // Retrieve the name from the state.
1194 
1195  // result = subposet_name(WHOLE_INDEX);
1196  result = _state->name();
1197  }
1198 
1199  // Postconditions:
1200 
1201  // Exit
1202 
1203  return result;
1204 }
1205 
1206 std::string
1208 name(bool xauto_access) const
1209 {
1210  string result;
1211 
1212  // Preconditions:
1213 
1214  require(is_external() ?
1215  name_space()->state_is_auto_read_accessible(xauto_access) :
1216  state_is_auto_read_accessible(xauto_access));
1217 
1218  // Body:
1219 
1220  if(xauto_access)
1221  {
1222  is_external() ? name_space()->get_read_access() : get_read_access();
1223  }
1224 
1225  result = name();
1226 
1227  if(xauto_access)
1228  {
1229  is_external() ? name_space()->release_access() : release_access();
1230  }
1231 
1232  // Postconditions:
1233 
1234  // Exit
1235 
1236  return result;
1237 }
1238 
1241 path(bool xauto_access) const
1242 {
1243 
1244  // Preconditions:
1245 
1246  require(is_external() ?
1247  name_space()->state_is_auto_read_accessible(xauto_access) :
1248  state_is_auto_read_accessible(xauto_access));
1249 
1250  // Body:
1251 
1252  poset_path result(name(xauto_access));
1253 
1254  // Postconditions:
1255 
1256  ensure(!result.empty());
1257  ensure(!result.full());
1258 
1259  // Exit:
1260 
1261  return result;
1262 }
1263 
1264 // PROTECTED FUNCTIONS
1265 
1266 void
1268 initialize_namespace(namespace_poset& xns, const std::string& xposet_name, bool xauto_link)
1269 {
1270  // Preconditions:
1271 
1272  require(state_is_read_accessible());
1273 
1278 
1279 
1280  // require(xns.contains_member(name()) ?
1281  // xns.state_is_read_write_accessible() :
1282  // xns.in_jim_edit_mode());
1283 
1284  require(xns.state_is_read_write_accessible());
1285 
1286  // Body:
1287 
1288  // Insert this into the namespace and
1289  // set the namespace and index features.
1290 
1291  disable_invariant_check();
1292 
1293  _name_space = &xns;
1294  _index = xns.insert_poset(*this, xposet_name, xauto_link, true);
1295 
1296  enable_invariant_check();
1297 
1298  // Postconditions:
1299 
1300  ensure(name_space() == &xns);
1301  ensure(name_space()->contains_member(index(), false));
1302  ensure(&name_space()->member_poset(index()) == this);
1303 
1304  // Exit
1305 
1306  return;
1307 }
1308 
1309 // PRIVATE FUNCTIONS
1310 
1311 // ===========================================================
1312 // POSET ALGEBRA FACET
1313 // ===========================================================
1314 
1315 // PUBLIC FUNCTIONS
1316 
1317 // PROTECTED FUNCTIONS
1318 
1319 // PRIVATE FUNCTIONS
1320 
1321 
1322 // ===========================================================
1323 // MEMBERSHIP FACET
1324 // ===========================================================
1325 
1326 // PUBLIC FUNCTIONS
1327 
1328 
1331 new_member(bool xis_jim, pod_index_type xtuple_hub_id)
1332 {
1333  // Preconditions:
1334 
1335  require(xis_jim ? in_jim_edit_mode() : state_is_read_write_accessible());
1336  require((!is_valid(xtuple_hub_id)) || contains_row_dof_tuple(xtuple_hub_id));
1337 
1338  // Body:
1339 
1340  // Member_ct and member_index_ub requires access to handle data mmembers in descendants,
1341  // which may no be attached yet. Also, see comment on postcondition.
1342  // define_old_variable(const scoped_index& old_member_index_ub = crg().end());
1343  // define_old_variable(int old_member_ct = member_ct());
1344 
1345  // Create new node in crg; ensures lower and upper covers empty.
1346 
1347  pod_index_type result = crg().new_member();
1348 
1349  // Set the dof tuple id for the member.
1350 
1351  crg().put_member_dof_tuple_id(result, xtuple_hub_id);
1352 
1353  // If node allocation has extended the member pool,
1354  // extend the subposet characteristic functions to match.
1355 
1356  if(crg().end() > powerset().subposet_member_index_ub())
1357  {
1358  powerset().put_subposet_member_index_ub(crg().end());
1359  }
1360 
1361  // Put new node in subposet of all members.
1362 
1363  powerset().whole().insert_member(result);
1364 
1365  // New members are not jims, not resident, and not modified by default.
1366  // Note that since resident and modified refers to the dof tuple,
1367  // and jrms don't have dof tuples, jrms should never be resident or modified.
1368 
1369  if(xis_jim)
1370  {
1371  // Put new member in subposet of all jims.
1372 
1373  jims().insert_member(result);
1374  }
1375 
1376  // Postconditions:
1377 
1378  ensure(invariant());
1379  ensure(cover_is_empty(LOWER, result));
1380  ensure(cover_is_empty(UPPER, result));
1381 
1382  // The following postconditions seems obvious, but it is not
1383  // true for immutable posets such as section_space_schema_poset.
1384  // ensure(member_ct() == (old_member_ct + 1));
1385 
1386  // Exit
1387 
1388  return result;
1389 }
1390 
1391 void
1393 new_member(bool xis_jim, const scoped_index& xtuple_id, scoped_index& result)
1394 {
1395  // Preconditions:
1396 
1397  require(xis_jim ? in_jim_edit_mode() : state_is_read_write_accessible());
1398  require(contains_row_dof_tuple(xtuple_id) || (!xtuple_id.is_valid()));
1399 
1400  // Body:
1401 
1402  result.put(member_hub_id_space(false), new_member(xis_jim, xtuple_id.hub_pod()));
1403 
1404  // Postconditions:
1405 
1406  ensure(invariant());
1407  ensure(cover_is_empty(LOWER, result));
1408  ensure(cover_is_empty(UPPER, result));
1409 
1410  // The following postconditions seems obvious, but it is not
1411  // true for immutable posets such as section_space_schema_poset.
1412  // ensure(member_ct() == (old_member_ct + 1));
1413 
1414  // Exit
1415 
1416  return;
1417 }
1418 
1421 new_member(bool xis_jim, poset_dof_map* xdof_map, bool xcopy_dof_map)
1422 {
1423  // Preconditions:
1424 
1425  require(xis_jim ? in_jim_edit_mode() : state_is_read_write_accessible());
1426  require(xdof_map != 0 ? xdof_map->host()->schema().is_same_state(&(schema())) : true);
1427  // schema is not attached yet when creating std members in namespace_poset, primitive_poset, etc.
1429 
1430  // Body:
1431 
1432  // Member_ct requires access to handle data mmembers in descendants,
1433  // which may no be attached yet. Also, see comment on postcondition.
1434  // define_old_variable(int old_member_ct = member_ct());
1435 
1436  // Get a dof tuple id.
1437 
1438  scoped_index ldof_map_id;
1439  if(!xis_jim)
1440  {
1441  // This member is a jrm, does not have a dof map.
1442 
1443  ldof_map_id.invalidate();
1444  ldof_map_id.put_scope(dof_tuple_hub_id_space(false));
1445  }
1446  else if(xdof_map == 0)
1447  {
1448  // This member is a jim, but client has not provided a dof map.
1449 
1450  // Create a new dof map.
1451 
1452  ldof_map_id = new_row_dof_map();
1453  }
1454  else if(xcopy_dof_map || !(xdof_map->host()->is_same_state(this)))
1455  {
1456  // This member is a jim and client has provided a dof map,
1457  // but has requested it be copied, or it is from another host
1458  // and must be copied.
1459 
1460  // Copy the client-provided dof map.
1461 
1462  ldof_map_id = clone_row_dof_map(*xdof_map);
1463  }
1464  else if(!(xdof_map->index().is_valid()))
1465  {
1466  // This member is a jim and client has provided a dof tuple
1467  // from this host, but it has not yet been entered in the table.
1468 
1469  // Put it in the table.
1470 
1471  table().put_row_dof_tuple(xdof_map);
1472  ldof_map_id = xdof_map->index(); // set by put_row_dof_tuple
1473  }
1474  else
1475  {
1476  // This member is a jim and client has provided a dof tuple
1477  // from this host and it is already in the table.
1478 
1479  // Just use it.
1480 
1481  ldof_map_id = xdof_map->index();
1482  }
1483 
1484  // Create the new member.
1485 
1486  pod_index_type result = new_member(xis_jim, ldof_map_id.hub_pod());
1487 
1488  // Postconditions:
1489 
1490  ensure(invariant());
1491  ensure(cover_is_empty(LOWER, result));
1492  ensure(cover_is_empty(UPPER, result));
1493 
1494  // The following postcondition seems obvious, but it is not
1495  // true for immutable posets such as section_space_schema_poset.
1496  // ensure(member_ct() == (old_member_ct + 1));
1497 
1498 
1499  // Exit
1500 
1501  return result;
1502 }
1503 
1504 void
1506 new_member(bool xis_jim, poset_dof_map* xdof_map, bool xcopy_dof_map, scoped_index& result)
1507 {
1508  // Preconditions:
1509 
1510  require(xis_jim ? in_jim_edit_mode() : state_is_read_write_accessible());
1511  require(xdof_map != 0 ? xdof_map->host()->schema().is_same_state(&(schema())) : true);
1512  // schema is not attached yet when creating std members in namespace_poset, primitive_poset, etc.
1514 
1515  // Body:
1516 
1517  result.put(member_hub_id_space(false), new_member(xis_jim, xdof_map, xcopy_dof_map));
1518 
1519  // Postconditions:
1520 
1521  ensure(invariant());
1522  ensure(cover_is_empty(LOWER, result));
1523  ensure(cover_is_empty(UPPER, result));
1524 
1525  // The following postcondition seems obvious, but it is not
1526  // true for immutable posets such as section_space_schema_poset.
1527  // ensure(member_ct() == (old_member_ct + 1));
1528 
1529  // Exit
1530 
1531  return;
1532 }
1533 
1536 new_member_interval(const std::string& xinterval_type,
1537  size_type xsize,
1538  const block<pod_index_type>& xtuple_hub_ids,
1539  const block<pod_index_type>& xdata)
1540 {
1541  // Preconditions:
1542 
1543  require(in_jim_edit_mode());
1544  require(implicit_crg_interval::interval_factory().contains_prototype(xinterval_type));
1545  require(xsize > 0);
1546 
1547  // Body:
1548 
1549  define_old_variable(const scoped_index old_member_index_ub = member_index_ub());
1550  define_old_variable(size_type old_member_ct = member_ct());
1551 
1552  pod_index_type result = new_member_interval(xinterval_type, xsize);
1553 
1554  implicit_crg_interval& linterval = *crg().implicit_member(result);
1555 
1556  linterval.initialize_dof_tuple_ids(xtuple_hub_ids);
1557  linterval.put_private_data(xdata);
1558  linterval.finalize(*this);
1559 
1560  // Postconditions:
1561 
1562  ensure(member_index_ub() >= old_member_index_ub + xsize);
1563  ensure(member_ct() == old_member_ct + xsize);
1564  ensure_for_range(pod_index_type i=result, i<member_index_ub().pod(), ++i, contains_member(i));
1565  ensure(unexecutable("result is_initialized()"));
1566 
1567  // Exit:
1568 
1569  return result;
1570 }
1571 
1572 void
1574 new_member_interval(const std::string& xinterval_type,
1575  size_type xsize,
1576  const block<pod_index_type>& xtuple_hub_ids,
1577  const block<pod_index_type>& xdata,
1578  scoped_index& result)
1579 {
1580  // Preconditions:
1581 
1582  require(in_jim_edit_mode());
1583  require(implicit_crg_interval::interval_factory().contains_prototype(xinterval_type));
1584  require(xsize > 0);
1585 
1586  // Body:
1587 
1588  define_old_variable(const scoped_index old_member_index_ub = member_index_ub());
1589  define_old_variable(size_type old_member_ct = member_ct());
1590 
1591  result.put(member_hub_id_space(false),
1592  new_member_interval(xinterval_type, xsize, xtuple_hub_ids, xdata));
1593 
1594  // Postconditions:
1595 
1596  ensure(member_index_ub() >= old_member_index_ub + xsize);
1597  ensure(member_ct() == old_member_ct + xsize);
1598  ensure_for_range(scoped_index i=result, i<member_index_ub(), ++i, contains_member(i));
1599  ensure(unexecutable("result is_initialized()"));
1600 
1601  // Exit:
1602 
1603  return;
1604 }
1605 
1606 void
1609 {
1610  // Preconditions:
1611 
1612  require(state_is_read_write_accessible());
1613  require(contains_member(xmbr_hub_id, false));
1614 
1617 
1618  // Body:
1619 
1620  // Delete the members name, if any, from the name map.
1621 
1622  delete_all_member_names(xmbr_hub_id, false);
1623 
1624  // Remove member from all subposets.
1625 
1626  powerset().delete_poset_member(xmbr_hub_id);
1627 
1628  // Clear cover sets, delete node in crg and the id from the top id space.
1629 
1630  crg().delete_member(xmbr_hub_id);
1631 
1632  // Postconditions:
1633 
1634  ensure(invariant());
1635  ensure(!contains_member(xmbr_hub_id, false));
1636  ensure(unexecutable(member_ct() = old member_ct() - 1));
1637  ensure(unexecutable("for all subposets s( !s.contains_member(xindex))"));
1638 
1639  // Exit
1640 
1641  return;
1642 }
1643 
1644 void
1647 {
1648  // Preconditions:
1649 
1650  require(state_is_read_write_accessible());
1651  require(contains_member(xmbr_id, false));
1652 
1655 
1656  // Body:
1657 
1658  delete_member(xmbr_id.hub_pod());
1659 
1660  // Postconditions:
1661 
1662  ensure(invariant());
1663  ensure(!contains_member(xmbr_id, false));
1664  ensure(unexecutable(member_ct() = old member_ct() - 1));
1665  ensure(unexecutable("for all subposets s( !s.contains_member(xindex))"));
1666 
1667  // Exit
1668 
1669  return;
1670 }
1671 
1672 int
1674 member_ct() const
1675 {
1676 
1677  // Preconditions:
1678 
1679  require(state_is_read_accessible());
1680 
1681  // Body:
1682 
1683  int result = crg().member_ct();
1684 
1685  // Postconditions:
1686 
1687  ensure(result >= 0);
1688 
1689  return result;
1690 }
1691 
1692 int
1695 {
1696  int result;
1697 
1698  // Preconditions:
1699 
1700  require(state_is_read_accessible());
1701 
1702  // Body:
1703 
1704  result = crg().standard_member_ct();
1705 
1706  // Postconditions:
1707 
1708  ensure(result >= 0);
1709 
1710  return result;
1711 }
1712 
1713 bool
1716 {
1717  bool result;
1718 
1719  // Preconditions:
1720 
1721  require(state_is_read_accessible());
1722 
1723  // Body:
1724 
1725  result = (member_ct() == standard_member_ct());
1726 
1727  // Postconditions:
1728 
1729  ensure(result == (member_ct() == standard_member_ct()));
1730 
1731  return result;
1732 }
1733 
1737 {
1738 
1739  // Preconditions:
1740 
1741  require(state_is_read_accessible());
1742 
1743  // Body:
1744 
1745  scoped_index result = crg().end();
1746 
1747  // Postconditions:
1748 
1749  ensure(result.is_hub_scope());
1750  ensure(result >= 0);
1751 
1752  return result;
1753 }
1754 
1758 {
1759  // Preconditions:
1760 
1761  require(state_is_read_accessible());
1762 
1763  // Body:
1764 
1765  index_iterator result(whole().members(), member_hub_id_space(false), false);
1766 
1767  // Postconditions:
1768 
1769  // Exit
1770 
1771  return result;
1772 }
1773 
1774 bool
1776 contains_member(pod_index_type xmbr_hub_id, bool xauto_access) const
1777 {
1778  // Preconditions:
1779 
1780  require(state_is_auto_read_accessible(xauto_access));
1781 
1782  if(xauto_access)
1783  {
1784  get_read_access();
1785  }
1786 
1787  // Body:
1788 
1789  bool result = crg().contains_member(xmbr_hub_id);
1790 
1791  // Postconditions:
1792 
1793  if(xauto_access)
1794  {
1795  release_access();
1796  }
1797 
1798  // Exit:
1799 
1800  return result;
1801 }
1802 
1803 bool
1805 contains_member(const scoped_index& xmbr_id, bool xauto_access) const
1806 {
1807  // Preconditions:
1808 
1809  require(xauto_access || state_is_read_accessible());
1810 
1811  // Body:
1812 
1813  return contains_member(xmbr_id.hub_pod(), xauto_access);
1814 }
1815 
1816 bool
1818 contains_member(pod_index_type xmbr_hub_id, int xversion, bool xauto_access) const
1819 {
1820  bool result;
1821 
1822  // Preconditions:
1823 
1824  require(state_is_auto_read_accessible(xauto_access));
1825 
1826  if(xauto_access)
1827  {
1828  get_read_access();
1829  }
1830 
1831  require(has_version(xversion));
1832 
1833  // Body:
1834 
1835  result = powerset().subposet_contains_member(version_index(xversion), xmbr_hub_id);
1836 
1837  // Postconditions:
1838 
1839  if(xauto_access)
1840  {
1841  release_access();
1842  }
1843 
1844  // Exit:
1845 
1846  return result;
1847 }
1848 
1849 bool
1851 contains_member(const scoped_index& xmbr_id, int xversion, bool xauto_access) const
1852 {
1853  bool result;
1854 
1855  // Preconditions:
1856 
1857  require(xauto_access || state_is_read_accessible());
1858  require(has_version(xversion));
1859 
1860  // Body:
1861 
1862  return contains_member(xmbr_id.hub_pod(), xversion, xauto_access);
1863 }
1864 
1865 bool
1867 contains_member(const std::string& xname, bool xauto_access) const
1868 {
1869  bool result;
1870 
1871  // Preconditions:
1872 
1873  require(state_is_auto_read_accessible(xauto_access));
1874 
1875  if(xauto_access)
1876  {
1877  get_read_access();
1878  }
1879 
1880  require(!xname.empty());
1881 
1882  // Body:
1883 
1884  // This particular implementation avoids the need for
1885  // redefining this function in the section_space_schema_poset classes.
1886 
1887  result = is_valid(member_id(xname, false));
1888 
1889  if(xauto_access)
1890  {
1891  release_access();
1892  }
1893 
1894  return result;
1895 }
1896 
1897 bool
1899 contains_member(const abstract_poset_member* xmbr, bool xauto_access) const
1900 {
1901 
1902  // Preconditions:
1903 
1904  require(xmbr != 0);
1905  require(xauto_access || state_is_read_accessible());
1906 
1907  // Body:
1908 
1909  bool result =
1910  is_same_state(xmbr->host()) && contains_member(xmbr->index(), xauto_access);
1911 
1912  // Postconditions:
1913 
1914  return result;
1915 }
1916 
1917 bool
1919 contains_members(const scoped_index* xmbrs, int xmbrs_ct, bool xauto_access) const
1920 {
1921 
1922  // Preconditions:
1923 
1924  require(xmbrs != 0);
1925  require(state_is_auto_read_accessible(xauto_access));
1926 
1927  // Body:
1928 
1929  if(xauto_access)
1930  {
1931  get_read_access();
1932  }
1933 
1934  bool result = true;
1935  int i = 0;
1936 
1937  while(result && i < xmbrs_ct)
1938  {
1939  result = contains_member(xmbrs[i], false);
1940  i++;
1941  };
1942 
1943  if(xauto_access)
1944  {
1945  release_access();
1946  }
1947 
1948  // Postconditions:
1949 
1950  ensure(unexecutable("result == for all i in xmbrs( contains_member(i) )"));
1951 
1952  // Exit
1953 
1954  return result;
1955 }
1956 
1957 bool
1959 contains_members(pod_index_type* xmbrs, int xmbrs_ct, bool xauto_access) const
1960 {
1961 
1962  // Preconditions:
1963 
1964  require(xmbrs != 0);
1965  require(state_is_auto_read_accessible(xauto_access));
1966 
1967  // Body:
1968 
1969  if(xauto_access)
1970  {
1971  get_read_access();
1972  }
1973 
1974  bool result = true;
1975  int i = 0;
1976 
1977  while(result && i < xmbrs_ct)
1978  {
1979  result = contains_member(xmbrs[i], false);
1980  i++;
1981  };
1982 
1983  if(xauto_access)
1984  {
1985  release_access();
1986  }
1987 
1988  // Postconditions:
1989 
1990  ensure(unexecutable("result == for all i in xmbrs( contains_member(i) )"));
1991 
1992  // Exit
1993 
1994  return result;
1995 }
1996 
1997 bool
1999 contains_members(const block<pod_index_type>& xmbrs, bool xauto_access) const
2000 {
2001 
2002  // Preconditions:
2003 
2004  require(state_is_auto_read_accessible(xauto_access));
2005 
2006  // Body:
2007 
2008  if(xauto_access)
2009  {
2010  get_read_access();
2011  }
2012 
2013  bool result = true;
2014  int i = 0;
2015 
2016  while(result && i < xmbrs.ct())
2017  {
2018  result = contains_member(xmbrs[i], false);
2019 
2020  i++;
2021  };
2022 
2023  if(xauto_access)
2024  {
2025  release_access();
2026  }
2027 
2028  // Postconditions:
2029 
2030  ensure(unexecutable("result == for all i in xmbrs( contains_member(i))"));
2031 
2032  // Exit
2033 
2034  return result;
2035 }
2036 
2037 bool
2039 contains_members(const block<scoped_index>& xmbrs, bool xauto_access) const
2040 {
2041 
2042  // Preconditions:
2043 
2044  require(state_is_auto_read_accessible(xauto_access));
2045 
2046  // Body:
2047 
2048  if(xauto_access)
2049  {
2050  get_read_access();
2051  }
2052 
2053  bool result = true;
2054  int i = 0;
2055 
2056  while(result && i < xmbrs.ct())
2057  {
2058  result = contains_member(xmbrs[i], false);
2059 
2060  i++;
2061  };
2062 
2063  if(xauto_access)
2064  {
2065  release_access();
2066  }
2067 
2068  // Postconditions:
2069 
2070  ensure(unexecutable("result == for all i in xmbrs( contains_member(i))"));
2071 
2072  // Exit
2073 
2074  return result;
2075 }
2076 
2077 bool
2079 contains_members(const std::string* xnames, int xnames_ct, bool xauto_access) const
2080 {
2081 
2082  // Preconditions:
2083 
2084  require(xnames != 0);
2085  require_for_all(i, 0, xnames_ct, !xnames[i].empty());
2086  require(state_is_auto_read_accessible(xauto_access));
2087 
2088  // Body:
2089 
2090  if(xauto_access)
2091  {
2092  get_read_access();
2093  }
2094 
2095  bool result = true;
2096  int i = 0;
2097 
2098  while(result && i < xnames_ct)
2099  {
2100  result = contains_member(xnames[i], false);
2101  i++;
2102  };
2103 
2104  if(xauto_access)
2105  {
2106  release_access();
2107  }
2108 
2109  // Postconditions:
2110 
2111  ensure(unexecutable("result == for all i in xnames( contains_member(xnames[i]))"));
2112 
2113  // Exit
2114 
2115  return result;
2116 }
2117 
2118 bool
2120 contains_members(const block<std::string>& xmbrs, bool xauto_access) const
2121 {
2122 
2123  // Preconditions:
2124 
2125  require_for_all(i, 0, xmbrs.ct(), !xmbrs[i].empty());
2126  require(state_is_auto_read_accessible(xauto_access));
2127 
2128  // Body:
2129 
2130  if(xauto_access)
2131  {
2132  get_read_access();
2133  }
2134 
2135  bool result = true;
2136  int i = 0;
2137 
2138  while(result && i < xmbrs.ct())
2139  {
2140  result = contains_member(xmbrs[i], false);
2141  i++;
2142  };
2143 
2144  if(xauto_access)
2145  {
2146  release_access();
2147  }
2148 
2149  // Postconditions:
2150 
2151  ensure(unexecutable("result == for all i in xmbrs( contains_member(xmbrs[i]) )"));
2152 
2153  // Exit
2154 
2155  return result;
2156 }
2157 
2158 bool
2160 is_empty() const
2161 {
2162  bool result;
2163 
2164  // Preconditions:
2165 
2166  require(state_is_read_accessible());
2167 
2168  // Body:
2169 
2170  result = member_ct() == 0;
2172 
2173  // Postconditions:
2174 
2175  // Exit
2176 
2177  return result;
2178 }
2179 
2180 bool
2182 is_jim(pod_index_type xmbr_hub_id, bool xin_current_version ) const
2183 {
2184  bool result;
2185 
2186  // Preconditions:
2187 
2188  require(state_is_read_accessible());
2189 
2190  // Body:
2191 
2192  if(xin_current_version)
2193  {
2194  // The member associated with xindex is a jim in the current
2195  // version if it is a member of the jims subposet.
2196 
2197  result = jims().contains_member(xmbr_hub_id);
2198  }
2199  else
2200  {
2201  // The member associated with xindex has a dof map if and only if
2202  // it is a jim in some version of the poset.
2203 
2204  result = is_valid(member_dof_tuple_id(xmbr_hub_id, false));
2205  }
2206 
2207  // Postconditions:
2208 
2209  // Exit
2210 
2211  return result;
2212 }
2213 
2214 bool
2216 is_jim(const scoped_index& xmbr_id, bool xin_current_version ) const
2217 {
2218  bool result;
2219 
2220  // Preconditions:
2221 
2222  require(state_is_read_accessible());
2223 
2224  // Body:
2225 
2226  return is_jim(xmbr_id.hub_pod(), xin_current_version);
2227 }
2228 
2229 bool
2231 is_jim(const std::string& xname, bool xin_current_version) const
2232 {
2233  bool result;
2234 
2235  // Preconditions:
2236 
2237  require(!xname.empty());
2238  require(state_is_read_accessible());
2239 
2240  // Body:
2241 
2242  pod_index_type lindex = member_id(xname, false);
2243  result = is_valid(lindex) && is_jim(lindex, xin_current_version);
2244 
2245  // Postconditions:
2246 
2247  // Exit
2248 
2249  return result;
2250 }
2251 
2252 bool
2254 is_atom(pod_index_type xmbr_hub_id) const
2255 {
2256  bool result;
2257 
2258  // Preconditions:
2259 
2260  require(state_is_read_accessible());
2261 
2262  // Body:
2263 
2264  result =
2265  (!cover_is_empty(LOWER, xmbr_hub_id)) &&
2266  (first_cover_member(LOWER, xmbr_hub_id) == BOTTOM_INDEX);
2267 
2268  // Postconditions:
2269 
2270  // Exit
2271 
2272  return result;
2273 }
2274 
2275 bool
2277 is_atom(const scoped_index& xmbr_id) const
2278 {
2279  bool result;
2280 
2281  // Preconditions:
2282 
2283  require(state_is_read_accessible());
2284 
2285  // Body:
2286 
2287  return is_atom(xmbr_id.hub_pod());
2288 }
2289 
2293 {
2294  // Preconditions:
2295 
2296  // Body:
2297 
2298  // Postconditions:
2299 
2300  // Exit
2301 
2302  return *_top;
2303 }
2304 
2307 top() const
2308 {
2309  // Preconditions:
2310 
2311  // Body:
2312 
2313  // Postconditions:
2314 
2315  // Exit
2316 
2317  return *_top;
2318 }
2319 
2323 {
2324  // Preconditions:
2325 
2326  // Body:
2327 
2328  // Postconditions:
2329 
2330  // Exit
2331 
2332  return *_bottom;
2333 }
2334 
2337 bottom() const
2338 {
2339  // Preconditions:
2340 
2341  // Body:
2342 
2343  // Postconditions:
2344 
2345  // Exit
2346 
2347  return *_bottom;
2348 }
2349 
2350 void
2353 {
2354  // Preconditions:
2355 
2356  require(state_is_read_write_accessible());
2357 
2358  // Body:
2359 
2360  // Enter jim edit mode.
2361 
2362  begin_jim_edit_mode(false);
2363 
2364  // Allocate the bottom member; becomes index 0.
2365  // No dof tuple allocated.
2366 
2367  bottom().attach_to_state(this, new_member(false));
2368  bottom().put_name("bottom", true, false);
2369 
2370  // Allocate the top member; becomes index 1.
2371  // No dof tuple allocated.
2372 
2373  top().attach_to_state(this, new_member(false));
2374  top().put_name("top", true, false);
2375 
2380 
2381  // Only two standard members and no dof tuples so far.
2382  // (More may be added in descendants.)
2383 
2384  // All the members and row dof tuples are standard.
2385 
2386  put_standard_member_ct(member_ct());
2387  put_standard_row_dof_tuple_ct(row_dof_tuple_ct());
2388 
2389  end_jim_edit_mode(true, false);
2390 
2391  // Now the cover relation graph invariant is satisfied
2392 
2393  crg().enable_invariant_check();
2394 
2395  assertion(crg().invariant());
2396 
2397  // Postconditions:
2398 
2399  ensure(bottom().is_attached() && (bottom().index() == BOTTOM_INDEX));
2400  ensure(top().is_attached() && (top().index() == TOP_INDEX));
2401  ensure(has_standard_member_ct());
2402  ensure(has_standard_row_dof_tuple_ct());
2403 
2404  // Exit
2405 
2406  return;
2407 }
2408 
2409 bool
2411 index_in_bounds(const scoped_index& xmbr_id) const
2412 {
2413  bool result;
2414 
2415  // Preconditions:
2416 
2417  require(state_is_read_accessible());
2418 
2419  // Body:
2420 
2421  result = xmbr_id.in_range(crg().begin(), crg().end());
2422 
2423  // Postconditions:
2424  ensure(invariant());
2425  ensure( result == xmbr_id.in_range(crg().begin(), crg().end()) );
2426 
2427  // Exit
2428 
2429  return(result);
2430 }
2431 
2432 bool
2434 index_in_bounds(const block<scoped_index>& xindices) const
2435 {
2436  bool result;
2437 
2438  // Preconditions:
2439 
2440  require(state_is_read_accessible());
2441 
2442  // Body:
2443 
2444  result = true;
2445  int i = 0;
2446  scoped_index lmember_index_ub = member_index_ub();
2447 
2448  while(i < xindices.ub() && result)
2449  {
2450  result = xindices[i].in_range(crg().begin(), crg().end()) && result;
2451  i++;
2452  };
2453 
2454  // Postconditions:
2455  ensure(invariant());
2456 
2457  // Exit
2458 
2459  return(result);
2460 }
2461 
2462 void
2464 new_member(pod_index_type xmbr_hub_id, bool xis_jim, const scoped_index& xdof_tuple_id)
2465 {
2466  // Preconditions:
2467 
2468  require(is_valid(xmbr_hub_id));
2469  require(!contains_member(xmbr_hub_id));
2470  require(xis_jim ? in_jim_edit_mode() : state_is_read_write_accessible());
2471  require(member_id_spaces(false).is_valid_reserved_id(xmbr_hub_id));
2472  require((!xdof_tuple_id.is_valid()) || contains_row_dof_tuple(xdof_tuple_id));
2473 
2474  // Body:
2475 
2476  define_old_variable(const scoped_index old_member_index_ub = member_index_ub());
2477  define_old_variable(int old_member_ct = member_ct());
2478 
2479  // Create new node in crg; ensures lower and upper covers empty.
2480 
2481  crg().new_member(xmbr_hub_id);
2482 
2483  // Set the dof tuple id for the member.
2484 
2485  crg().put_member_dof_tuple_id(xmbr_hub_id, xdof_tuple_id.hub_pod());
2486 
2487  // If node allocation has extended the member pool,
2488  // extend the subposet characteristic functions to match.
2489 
2490  if(crg().end() > powerset().subposet_member_index_ub())
2491  {
2492  powerset().put_subposet_member_index_ub(crg().end());
2493  }
2494 
2495  // Put new node in subposet of all members.
2496 
2497  powerset().whole().insert_member(xmbr_hub_id);
2498 
2499  // New members are not jims, not resident, and not modified by default.
2500  // Note that since resident and modified refers to the dof tuple,
2501  // and jrms don't have dof tuples, jrms should never be resident or modified.
2502 
2503  if(xis_jim)
2504  {
2505  // Put new member in subposet of all jims.
2506 
2507  jims().insert_member(xmbr_hub_id);
2508  }
2509 
2510  // Postconditions:
2511 
2512  ensure(invariant());
2513  ensure(contains_member(xmbr_hub_id));
2514  ensure(cover_is_empty(LOWER, xmbr_hub_id));
2515  ensure(cover_is_empty(UPPER, xmbr_hub_id));
2516 
2517  // The following postconditions seems obvious, but it is not
2518  // true for immutable posets such as section_space_schema_poset.
2519  // ensure(member_ct() == (old_member_ct + 1));
2520 
2521  // Exit
2522 
2523  return;
2524 }
2525 
2526 void
2528 new_member(pod_index_type xmbr_hub_id, bool xis_jim, poset_dof_map* xdof_map, bool xcopy_dof_map)
2529 {
2530  // Preconditions:
2531 
2532  require(is_valid(xmbr_hub_id));
2533  require(!contains_member(xmbr_hub_id));
2534  require(xis_jim ? in_jim_edit_mode() : state_is_read_write_accessible());
2535  require(member_id_spaces(false).is_valid_reserved_id(xmbr_hub_id));
2536  require(xdof_map != 0 ? xdof_map->host()->schema().is_same_state(&(schema())) : true);
2537  // schema is not attached yet when creating std members in namespace_poset, primitive_poset, etc.
2539 
2540  // Body:
2541 
2542  define_old_variable(int old_member_ct = member_ct());
2543 
2544  // Get a dof tuple id.
2545 
2546  scoped_index ldof_map_id(dof_tuple_hub_id_space(false));
2547  if(!xis_jim)
2548  {
2549  // This member is a jrm, does not have a dof map.
2550 
2551  ldof_map_id.invalidate();
2552  }
2553  else if(xdof_map == 0)
2554  {
2555  // This member is a jim, but client has not provided a dof map.
2556 
2557  // Create a new dof map.
2558 
2559  ldof_map_id = new_row_dof_map();
2560  }
2561  else if(xcopy_dof_map || !(xdof_map->host()->is_same_state(this)))
2562  {
2563  // This member is a jim and client has provided a dof map,
2564  // but has requested it be copied, or it is from another host
2565  // and must be copied.
2566 
2567  // Copy the client-provided dof map.
2568 
2569  ldof_map_id = clone_row_dof_map(*xdof_map);
2570  }
2571  else if(!(xdof_map->index().is_valid()))
2572  {
2573  // This member is a jim and client has provided a dof tuple
2574  // from this host, but it has not yet been entered in the table.
2575 
2576  // Put it in the table.
2577 
2578  table().put_row_dof_tuple(xdof_map);
2579  ldof_map_id = xdof_map->index(); // set by put_row_dof_tuple
2580  }
2581  else
2582  {
2583  // This member is a jim and client has provided a dof tuple
2584  // from this host and it is already in the table.
2585 
2586  // Just use it.
2587 
2588  ldof_map_id = xdof_map->index();
2589  }
2590 
2591  // Create the new member.
2592 
2593  new_member(xmbr_hub_id, xis_jim, const_cast<const scoped_index&>(ldof_map_id));
2594 
2595  // Postconditions:
2596 
2597  ensure(invariant());
2598  ensure(contains_member(xmbr_hub_id));
2599  ensure(cover_is_empty(LOWER, xmbr_hub_id));
2600  ensure(cover_is_empty(UPPER, xmbr_hub_id));
2601 
2602  // The following postcondition seems obvious, but it is not
2603  // true for immutable posets such as section_space_schema_poset.
2604  // ensure(member_ct() == (old_member_ct + 1));
2605 
2606 
2607  // Exit
2608 
2609  return;
2610 }
2611 
2614 new_member_interval(const std::string& xinterval_type, size_type xsize)
2615 {
2616  // Preconditions:
2617 
2618  require(in_jim_edit_mode());
2619  require(implicit_crg_interval::interval_factory().contains_prototype(xinterval_type));
2620  require(xsize > 0);
2621 
2622  // Body:
2623 
2624  define_old_variable(const scoped_index old_member_index_ub = member_index_ub());
2625  define_old_variable(size_type old_member_ct = member_ct());
2626 
2627  // Allocate the interval in the member id space
2628  // and create the member emulator for it.
2629 
2630  pod_index_type result = crg().new_member_interval(xinterval_type, xsize);
2631  implicit_crg_interval& linterval = *crg().implicit_member(result);
2632 
2633  // If node allocation has extended the member pool,
2634  // extend the subposet characteristic functions to match.
2635 
2636  if(crg().end() > powerset().subposet_member_index_ub())
2637  {
2638  powerset().put_subposet_member_index_ub(crg().end());
2639  }
2640 
2641  for(pod_index_type i=linterval.begin(); i<linterval.end(); ++i)
2642  {
2643  // Set whole() membership.
2644 
2645  powerset().whole().insert_member(i);
2646  }
2647 
2648  // Postconditions:
2649 
2650  ensure(member_index_ub() >= old_member_index_ub + xsize);
2651  ensure(member_ct() == old_member_ct + xsize);
2652  ensure_for_range(pod_index_type i=result, i<member_index_ub().pod(), ++i, contains_member(i));
2653  ensure(unexecutable("result size_initialized()"));
2654  ensure(unexecutable("result local_id_space_initialized()"));
2655 
2656  // Exit:
2657 
2658  return result;
2659 }
2660 
2661 void
2663 new_member_interval(pod_index_type xmbr_hub_id, const std::string& xinterval_type, size_type xsize)
2664 {
2665  // Preconditions:
2666 
2667  require(is_valid(xmbr_hub_id));
2668  require_for_range(pod_index_type i=0, i<xsize, ++i, !contains_member(xmbr_hub_id + i));
2669  require(in_jim_edit_mode());
2670  require(implicit_crg_interval::interval_factory().contains_prototype(xinterval_type));
2671  require(xsize > 0);
2672 
2673  // Body:
2674 
2675  define_old_variable(const scoped_index old_member_index_ub = member_index_ub());
2676  define_old_variable(size_type old_member_ct = member_ct());
2677 
2678  // Allocate the interval in the member id space
2679  // and create the member emulator for it.
2680 
2681  crg().new_member_interval(xmbr_hub_id, xinterval_type, xsize);
2682  implicit_crg_interval& linterval = *crg().implicit_member(xmbr_hub_id);
2683 
2684  // If node allocation has extended the member pool,
2685  // extend the subposet characteristic functions to match.
2686 
2687  if(crg().end() > powerset().subposet_member_index_ub())
2688  {
2689  powerset().put_subposet_member_index_ub(crg().end());
2690  }
2691 
2692  for(pod_index_type i=linterval.begin(); i<linterval.end(); ++i)
2693  {
2694  // Set whole() membership.
2695 
2696  powerset().whole().insert_member(i);
2697  }
2698 
2699  // Postconditions:
2700 
2701  ensure(member_index_ub() >= old_member_index_ub);
2702  ensure(member_ct() == old_member_ct + xsize);
2703  ensure_for_range(pod_index_type i=0, i<xsize, ++i, contains_member(xmbr_hub_id + i));
2704  ensure(unexecutable("result size_initialized()"));
2705  ensure(unexecutable("result local_id_space_initialized()"));
2706 
2707  // Exit:
2708 
2709  return;
2710 }
2711 
2712 // PRIVATE FUNCTIONS
2713 
2714 
2715 // ===========================================================
2716 // MEMBER NAME FACET
2717 // ===========================================================
2718 
2719 // PUBLIC MEMBER FUNCTIONS
2720 
2723 member_path(pod_index_type xmbr_hub_id, bool xauto_access) const
2724 {
2725  // cout << endl << "Entering poset_state_handle::member_path." << endl;
2726 
2727  // Preconditions:
2728 
2729  require(state_is_auto_read_accessible(xauto_access));
2730  require(contains_member(xmbr_hub_id, xauto_access));
2731 
2732  // Body:
2733 
2734  poset_path result(name(xauto_access), member_name(xmbr_hub_id, xauto_access));
2735 
2736  // Postconditions:
2737 
2738  ensure(result.poset_name() == name(xauto_access));
2739  ensure(member_id(result.member_name(), xauto_access) == xmbr_hub_id);
2740 
2741  // Exit:
2742 
2743  // cout << "Leaving poset_state_handle::member_path." << endl;
2744  return result;
2745 }
2746 
2747 
2748 std::string
2750 member_name(pod_index_type xmbr_hub_id, bool xauto_access) const
2751 {
2752  // Preconditions:
2753 
2754  require(state_is_auto_read_accessible(xauto_access));
2755 
2756  // Body:
2757 
2758  if(xauto_access)
2759  {
2760  get_read_access();
2761  }
2762 
2763  string result(crg().member_name_map().name(xmbr_hub_id));
2764 
2765  if(xauto_access)
2766  {
2767  release_access();
2768  }
2769 
2770  // Exit:
2771 
2772  return result;
2773 }
2774 
2775 std::string
2777 member_name(const scoped_index& xmbr_id, bool xauto_access) const
2778 {
2779  // Preconditions:
2780 
2781  require(xauto_access || state_is_read_accessible());
2782 
2783  // Body:
2784 
2785  return member_name(xmbr_id.hub_pod(), xauto_access);
2786 }
2787 
2788 void
2791  block<std::string>& xresult,
2792  bool xauto_access) const
2793 {
2794  // Preconditions:
2795 
2796  require(state_is_auto_read_accessible(xauto_access));
2797  require(contains_member(xmbr_hub_id, xauto_access));
2798 
2799  // Body:
2800 
2801  if(xauto_access)
2802  {
2803  get_read_access();
2804  }
2805 
2806  crg().member_name_map().all_names(xmbr_hub_id, xresult);
2807 
2808  if(xauto_access)
2809  {
2810  release_access();
2811  }
2812 
2813  // Postconditions:
2814 
2815  ensure(xresult.ct() == member_name_ct(xmbr_hub_id, xauto_access));
2816  ensure_for_all(i, 0, xresult.ct(), member_has_name(xmbr_hub_id, xresult[i], xauto_access));
2817 
2818  // Exit:
2819 
2820  return;
2821 }
2822 
2823 void
2826  block<std::string>& xresult,
2827  bool xauto_access) const
2828 {
2829  // Preconditions:
2830 
2831  require(xauto_access || state_is_read_accessible());
2832  require(contains_member(xmbr_id, xauto_access));
2833 
2834  // Body:
2835 
2836  all_member_names(xmbr_id.hub_pod(), xresult, xauto_access);
2837 
2838  // Postconditions:
2839 
2840  ensure(xresult.ct() == member_name_ct(xmbr_id, xauto_access));
2841  ensure_for_all(i, 0, xresult.ct(), member_has_name(xmbr_id, xresult[i], xauto_access));
2842 
2843  // Exit:
2844 
2845  return;
2846 }
2847 
2850 member_name_ct(pod_index_type xmbr_hub_id, bool xauto_access) const
2851 {
2852  size_type result;
2853 
2854  // Preconditions:
2855 
2856  require(state_is_auto_read_accessible(xauto_access));
2857  require(contains_member(xmbr_hub_id, xauto_access));
2858 
2859  // Body:
2860 
2861  if(xauto_access)
2862  {
2863  get_read_access();
2864  }
2865 
2866  result = crg().member_name_map().name_ct(xmbr_hub_id);
2867 
2868  if(xauto_access)
2869  {
2870  release_access();
2871  }
2872 
2873  // Postconditions:
2874 
2875  // Exit:
2876 
2877  return result;
2878 }
2879 
2882 member_name_ct(const scoped_index& xmbr_id, bool xauto_access) const
2883 {
2884  size_type result;
2885 
2886  // Preconditions:
2887 
2888  require(xauto_access || state_is_read_accessible());
2889  require(contains_member(xmbr_id, xauto_access));
2890 
2891  // Body:
2892 
2893  return member_name_ct(xmbr_id.hub_pod(), xauto_access);
2894 }
2895 
2896 bool
2898 member_has_name(pod_index_type xmbr_hub_id, const std::string& xname, bool xauto_access) const
2899 {
2900  // Preconditions:
2901 
2902  require(state_is_auto_read_accessible(xauto_access));
2903  require(!xname.empty());
2904  require(contains_member(xmbr_hub_id, xauto_access));
2905 
2906  // Body:
2907 
2908  if(xauto_access)
2909  {
2910  get_read_access();
2911  }
2912 
2913  bool result = crg().member_name_map().contains_entry(xmbr_hub_id, xname);
2914 
2915  if(xauto_access)
2916  {
2917  release_access();
2918  }
2919 
2920  // Postconditions:
2921 
2922  // Exit:
2923 
2924  return result;
2925 }
2926 
2927 bool
2929 member_has_name(const scoped_index& xmbr_id, const std::string& xname, bool xauto_access) const
2930 {
2931  // Preconditions:
2932 
2933  require(xauto_access || state_is_read_accessible());
2934  require(!xname.empty());
2935  require(contains_member(xmbr_id, xauto_access));
2936 
2937  // Body:
2938 
2939  return member_has_name(xmbr_id.hub_pod(), xname, xauto_access);
2940 }
2941 
2942 void
2945  const std::string& xname,
2946  bool xunique,
2947  bool xauto_access)
2948 {
2949  // Preconditions:
2950 
2951  require(state_is_auto_read_write_accessible(xauto_access));
2952  require(contains_member(xmbr_hub_id, xauto_access));
2953  require(poset_path::is_valid_name(xname));
2954 
2955  // Body:
2956 
2957  if(xauto_access)
2958  {
2959  get_read_write_access(true);
2960  }
2961 
2962  crg().member_name_map().put_entry(xmbr_hub_id, xname, xunique);
2963 
2964  if(xauto_access)
2965  {
2966  release_access();
2967  }
2968 
2969  // Postcondition:
2970 
2971  ensure(member_has_name(xmbr_hub_id, xname, xauto_access));
2972 
2973  // Exit
2974 
2975  return;
2976 }
2977 
2978 void
2981  const std::string& xname,
2982  bool xunique,
2983  bool xauto_access)
2984 {
2985  // Preconditions:
2986 
2987  require(xauto_access || state_is_read_write_accessible());
2988  require(contains_member(xmbr_id, xauto_access));
2989  require(poset_path::is_valid_name(xname));
2990 
2991  // Body:
2992 
2993  put_member_name(xmbr_id.hub_pod(), xname, xunique, xauto_access);
2994 
2995  // Postcondition:
2996 
2997  ensure(member_has_name(xmbr_id, xname, xauto_access));
2998 
2999  // Exit
3000 
3001  return;
3002 }
3003 
3004 void
3006 delete_member_name(const std::string& xname, bool xauto_access)
3007 {
3008  // Preconditions:
3009 
3010  require(!xname.empty());
3011  require(state_is_auto_read_write_accessible(xauto_access));
3012 
3013  // Body:
3014 
3015  if(xauto_access)
3016  {
3017  get_read_write_access(true);
3018  }
3019 
3020  crg().member_name_map().delete_name(xname);
3021 
3022  if(xauto_access)
3023  {
3024  release_access();
3025  }
3026 
3027  // Postcondition
3028 
3029  ensure(!contains_member(xname, xauto_access));
3030 
3031  // Exit:
3032 
3033  return;
3034 }
3035 
3036 void
3038 delete_all_member_names(pod_index_type xmbr_hub_id, bool xauto_access)
3039 {
3040  // Preconditions:
3041 
3042  require(state_is_auto_read_write_accessible(xauto_access));
3043 
3044  // Body:
3045 
3046  if(xauto_access)
3047  {
3048  get_read_write_access(true);
3049  }
3050 
3051  crg().member_name_map().delete_index(xmbr_hub_id);
3052 
3053  if(xauto_access)
3054  {
3055  release_access();
3056  }
3057 
3058  // Postcondition
3059 
3060  ensure(member_name_ct(xmbr_hub_id, xauto_access) == 0);
3061 
3062  // Exit:
3063 
3064  return;
3065 }
3066 
3067 void
3069 delete_all_member_names(const scoped_index& xmbr_id, bool xauto_access)
3070 {
3071  // Preconditions:
3072 
3073  require(xauto_access || state_is_read_write_accessible());
3074 
3075  // Body:
3076 
3077  delete_all_member_names(xmbr_id.hub_pod(), xauto_access);
3078 
3079  // Postcondition
3080 
3081  ensure(member_name_ct(xmbr_id, xauto_access) == 0);
3082 
3083  // Exit:
3084 
3085  return;
3086 }
3087 
3088 // PROTECTED MEMBER FUNCTIONS
3089 
3092 member_name_map(bool xrequire_write_access)
3093 {
3094  // Preconditions:
3095 
3096  require(xrequire_write_access ? state_is_read_write_accessible() : state_is_read_accessible());
3097 
3098  // Body:
3099 
3100  member_name_map_type& result = crg().member_name_map();
3101 
3102  // Postconditions:
3103 
3104  // Exit
3105 
3106  return result;
3107 }
3108 
3109 // PRIVATE MEMBER FUNCTIONS
3110 
3111 
3112 // ===========================================================
3113 // MEMBER ID SPACE FAMILY FACET
3114 // ===========================================================
3115 
3116 // PUBLIC FUNCTIONS
3117 
3120 member_id_spaces(bool xauto_access) const
3121 {
3122  // Preconditions:
3123 
3124  require(state_is_auto_read_accessible(xauto_access));
3125 
3126  // Body:
3127 
3128  if(xauto_access)
3129  {
3130  get_read_access();
3131  }
3132 
3133  const index_space_family& result = crg()._id_spaces;
3134 
3135  if(xauto_access)
3136  {
3137  release_access();
3138  }
3139 
3140  // Postconditions:
3141 
3142  ensure(is_basic_query);
3143 
3144  // Exit:
3145 
3146  return result;
3147 }
3148 
3151 member_id_spaces(bool xauto_access)
3152 {
3153  // Preconditions:
3154 
3155  require(state_is_auto_read_accessible(xauto_access));
3156 
3157  // Body:
3158 
3159  if(xauto_access)
3160  {
3161  get_read_access();
3162  }
3163 
3164  index_space_family& result = crg()._id_spaces;
3165 
3166  if(xauto_access)
3167  {
3168  release_access();
3169  }
3170 
3171  // Postconditions:
3172 
3173  ensure(is_basic_query);
3174 
3175  // Exit:
3176 
3177  return result;
3178 }
3179 
3182 member_hub_id_space(bool xauto_access) const
3183 {
3184  // Preconditions:
3185 
3186  require(state_is_auto_read_accessible(xauto_access));
3187 
3188  // Body:
3189 
3190  if(xauto_access)
3191  {
3192  get_read_access();
3193  }
3194 
3195  const hub_index_space_handle& result = crg().id_spaces().hub_id_space();
3196 
3197  if(xauto_access)
3198  {
3199  release_access();
3200  }
3201 
3202  // Postconditions:
3203 
3204  ensure(result.is_attached());
3205 
3206  // Exit:
3207 
3208  return result;
3209 }
3210 
3211 const sheaf::scoped_index&
3213 member_id(bool xauto_access) const
3214 {
3215  // Preconditions:
3216 
3217  require(state_is_auto_read_accessible(xauto_access));
3218 
3219  // Body:
3220 
3221  if(xauto_access)
3222  {
3223  get_read_access();
3224  }
3225 
3226  const scoped_index& result = crg().hub_id();
3227 
3228  if(xauto_access)
3229  {
3230  release_access();
3231  }
3232 
3233  // Postconditions:
3234 
3235  ensure(result.same_scope(member_hub_id_space(xauto_access)));
3236 
3237  // Exit:
3238 
3239  return result;
3240 }
3241 
3244 member_id(pod_index_type xid, bool xauto_access) const
3245 {
3246  // Preconditions:
3247 
3248  require(state_is_auto_read_accessible(xauto_access));
3249 
3250  // Body:
3251 
3252  if(xauto_access)
3253  {
3254  get_read_access();
3255  }
3256 
3257  scoped_index result(member_id(false));
3258  result = xid;
3259 
3260  if(xauto_access)
3261  {
3262  release_access();
3263  }
3264 
3265  // Postconditions:
3266 
3267  ensure(result.same_scope(member_hub_id_space(xauto_access)));
3268  ensure(result.pod() == xid);
3269 
3270  // Exit:
3271 
3272  return result;
3273 }
3274 
3277 member_id(const std::string& xname, bool xauto_access) const
3278 {
3279  // Preconditions:
3280 
3281  require(state_is_auto_read_accessible(xauto_access));
3282  require(!xname.empty());
3283 
3284  // Body:
3285 
3286  if(xauto_access)
3287  {
3288  get_read_access();
3289  }
3290 
3291  // Lookup the name in the name-to-index map.
3292 
3293  pod_index_type result = crg().member_name_map().index(xname);
3294 
3295  if(xauto_access)
3296  {
3297  release_access();
3298  }
3299 
3300  // Postcondition:
3301 
3302  ensure(is_valid(result) ? member_has_name(result, xname, xauto_access) : true);
3303 
3304  // Exit
3305 
3306  return result;
3307 }
3308 
3309 void
3311 member_id(const std::string& xname, scoped_index& result, bool xauto_access) const
3312 {
3313  // Preconditions:
3314 
3315  require(state_is_auto_read_accessible(xauto_access));
3316  require(!xname.empty());
3317 
3318  // Body:
3319 
3320  result.put(member_hub_id_space(xauto_access), member_id(xname, xauto_access));
3321 
3322  // Postcondition:
3323 
3324  ensure(result.is_valid() ? member_has_name(result, xname, xauto_access) : true);
3325 
3326  // Exit
3327 
3328  return;
3329 }
3330 
3331 // PROTECTED FUNCTIONS
3332 
3333 void
3336 {
3337  // Preconditions:
3338 
3339  require(state_is_read_write_accessible());
3340 
3341  // Body:
3342 
3343  crg()._id_spaces.update_standard_id_spaces();
3344 
3345  // Postconditions:
3346 
3347  // Exit:
3348 
3349  return;
3350 }
3351 
3352 void
3354 clear_member_id_spaces(bool xauto_access)
3355 {
3356  // Preconditions:
3357 
3358  require(state_is_auto_read_write_accessible(xauto_access));
3359 
3360  // Body:
3361 
3362  if(xauto_access)
3363  {
3364  get_read_write_access(true);
3365  }
3366 
3367  crg()._id_spaces.clear_id_spaces();
3368 
3369  // Postconditions:
3370 
3371  ensure(member_id_spaces(false).has_only_standard_id_spaces());
3372 
3373  if(xauto_access)
3374  {
3375  release_access();
3376  }
3377 
3378  // Exit:
3379 
3380  return;
3381 }
3382 
3383 void
3385 extend_last_member_term(size_type xct, bool xauto_access)
3386 {
3387  // Preconditions:
3388 
3389  require(state_is_auto_read_write_accessible(xauto_access));
3390  require(!member_hub_id_space(xauto_access).is_empty());
3391 
3392  // Body:
3393 
3394  if(xauto_access)
3395  {
3396  get_read_write_access();
3397  }
3398 
3399  define_old_variable(const index_space_handle& last_term = member_id_spaces(false).last_term());
3400  define_old_variable(scoped_index old_last_term_begin(last_term, last_term.begin()));
3401 
3402  if(xct > crg()._id_spaces.last_term().ct())
3403  {
3404  crg()._id_spaces.extend_last_term(xct);
3405  }
3406 
3407  if(xauto_access)
3408  {
3409  release_access();
3410  }
3411 
3412  // Postcondtions:
3413 
3414  ensure_for_range(scoped_index i=old_last_term_begin, i<old_last_term_begin+xct, ++i, i.in_scope());
3415 
3416  // Exit:
3417 
3418  return;
3419 }
3420 
3423 new_term(size_type xct, bool xauto_access)
3424 {
3425  // Preconditions:
3426 
3427  require(state_is_auto_read_write_accessible(xauto_access));
3428 
3429  // Body:
3430 
3431  if(xauto_access)
3432  {
3433  get_read_write_access();
3434  }
3435 
3436  pod_index_type result = crg()._id_spaces.new_primary_state(xct);
3437 
3438  if(xauto_access)
3439  {
3440  release_access();
3441  }
3442 
3443  // Postcondtions:
3444 
3445  // Exit:
3446 
3447  return result;
3448 }
3449 
3450 // PRIVATE FUNCTIONS
3451 
3452 
3453 // ===========================================================
3454 // ORDER RELATION FACET
3455 // ===========================================================
3456 
3457 // PUBLIC FUNCTIONS
3458 
3459 bool
3461 le(pod_index_type xgreater, pod_index_type xlesser) const
3462 {
3463  bool result = false;
3464 
3465  // Preconditions:
3466 
3467  require(state_is_read_accessible());
3468  require(contains_member(xlesser, false));
3469  require(contains_member(xgreater, false));
3470 
3471  // Body:
3472 
3473  result = xgreater == xlesser;
3474  if(!result)
3475  {
3476  // recur on upper cover
3478 
3479  index_space_iterator& itr = get_cover_id_space_iterator(UPPER, xlesser);
3480  while((!itr.is_done()) && !result)
3481  {
3482  result = le(xgreater, itr.hub_pod());
3483  itr.next();
3484  }
3485  release_cover_id_space_iterator(itr);
3486  }
3487 
3488  // Postconditions:
3489 
3490  ensure(unexecutable(upset of xlesser contains xgreater));
3491 
3492  // Exit
3493 
3494  return result;
3495 }
3496 
3497 bool
3499 le(const scoped_index& xgreater, const scoped_index& xlesser) const
3500 {
3501  bool result = false;
3502 
3503  // Preconditions:
3504 
3505  require(state_is_read_accessible());
3506  require(contains_member(xlesser, false));
3507  require(contains_member(xgreater, false));
3508 
3509  // Body:
3510 
3511  result = le(xgreater.hub_pod(), xlesser.hub_pod());
3512 
3513  // Postconditions:
3514 
3515  ensure(unexecutable(upset of xlesser contains xgreater));
3516 
3517  // Exit
3518 
3519  return result;
3520 }
3521 
3522 bool
3524 leqv(pod_index_type xgreater, pod_index_type xlesser) const
3525 {
3526  bool result = false;
3527 
3528  // Preconditions:
3529 
3530  require(state_is_read_accessible());
3531  require(contains_member(xlesser, false));
3532  require(contains_member(xgreater, false));
3533 
3534  // Body:
3535 
3536  result = le(xgreater, xlesser) || is_jem(xgreater, xlesser);
3537 
3538  // Postconditions:
3539 
3540  ensure(unexecutable(upset of xlesser contains xgreater));
3541 
3542  // Exit
3543 
3544  return result;
3545 }
3546 
3547 bool
3549 leqv(const scoped_index& xgreater, const scoped_index& xlesser) const
3550 {
3551  bool result = false;
3552 
3553  // Preconditions:
3554 
3555  require(state_is_read_accessible());
3556  require(contains_member(xlesser, false));
3557  require(contains_member(xgreater, false));
3558 
3559  // Body:
3560 
3561  result = leqv(xgreater.hub_pod(), xlesser.hub_pod());
3562 
3563  // Postconditions:
3564 
3565  ensure(unexecutable(upset of xlesser contains xgreater));
3566 
3567  // Exit
3568 
3569  return result;
3570 }
3571 
3572 bool
3574 is_jem(pod_index_type xmbr_hub_id, pod_index_type xother_hub_id) const
3575 {
3576  bool result;
3577 
3578  // Preconditions:
3579 
3580  require(state_is_read_accessible());
3581  require(contains_member(xmbr_hub_id, false));
3582  require(contains_member(xother_hub_id, false));
3583 
3584  // Body:
3585 
3586  result = (greatest_jem(xmbr_hub_id) == greatest_jem(xother_hub_id));
3587 
3588  // Postconditions:
3589 
3590  // Exit
3591 
3592  return result;
3593 }
3594 
3595 bool
3597 is_jem(const scoped_index& xmbr_id, const scoped_index& xother_id) const
3598 {
3599  bool result;
3600 
3601  // Preconditions:
3602 
3603  require(state_is_read_accessible());
3604  require(contains_member(xmbr_id, false));
3605  require(contains_member(xother_id, false));
3606 
3607  // Body:
3608 
3609  return is_jem(xmbr_id.hub_pod(), xother_id.hub_pod());
3610 }
3611 
3614 greatest_jem(pod_index_type xmbr_hub_id) const
3615 {
3616  // Preconditions:
3617 
3618  require(state_is_read_accessible());
3619  require(contains_member(xmbr_hub_id, false));
3620 
3621  // Body:
3622 
3623  pod_index_type result = xmbr_hub_id;
3624 
3625  pod_index_type lfirst_upper_mbr = invalid_pod_index();
3626  if(!cover_is_empty(UPPER, result))
3627  {
3628  lfirst_upper_mbr = first_cover_member(UPPER, result);
3629  }
3630 
3631 
3632  while(is_valid(lfirst_upper_mbr) &&
3633  !is_jim(lfirst_upper_mbr) &&
3634  cover_is_singleton(LOWER, lfirst_upper_mbr))
3635  {
3636  result = lfirst_upper_mbr;
3637  if(cover_is_empty(UPPER, lfirst_upper_mbr))
3638  {
3639  lfirst_upper_mbr = invalid_pod_index();
3640  }
3641  else
3642  {
3643  lfirst_upper_mbr = first_cover_member(UPPER, lfirst_upper_mbr);
3644  }
3645  }
3646 
3647  // Postconditions:
3648 
3649  // Exit
3650 
3651  return result;
3652 }
3653 
3654 void
3656 greatest_jem(const scoped_index& xmbr_id, scoped_index& result) const
3657 {
3658  // Preconditions:
3659 
3660  require(state_is_read_accessible());
3661  require(contains_member(xmbr_id, false));
3662 
3663  // Body:
3664 
3665  result.put(member_hub_id_space(false), greatest_jem(xmbr_id.hub_pod()));
3666 
3667  // Postconditions:
3668 
3669  // Exit
3670 
3671  return;
3672 }
3673 
3676 least_jem(pod_index_type xmbr_hub_id) const
3677 {
3678  // Preconditions:
3679 
3680  require(state_is_read_accessible());
3681  require(contains_member(xmbr_hub_id, false));
3682 
3683  // Body:
3684 
3685  pod_index_type result = xmbr_hub_id;
3686  while(!is_jim(result) && cover_is_singleton(LOWER, result))
3687  {
3688  result = first_cover_member(LOWER, result);
3689  }
3690 
3691  // Postconditions:
3692 
3693  ensure(is_jim(result) || !cover_is_singleton(LOWER, result));
3694  ensure(le(xmbr_hub_id, result));
3695 
3696  // Exit
3697 
3698  return result;
3699 }
3700 
3701 void
3703 least_jem(const scoped_index& xmbr_id, scoped_index& result) const
3704 {
3705  // Preconditions:
3706 
3707  require(state_is_read_accessible());
3708  require(contains_member(xmbr_id, false));
3709 
3710  // Body:
3711 
3712  result.put(member_hub_id_space(false), least_jem(xmbr_id.hub_pod()));
3713 
3714  // Postconditions:
3715 
3716  ensure(is_jim(result) || !cover_is_singleton(LOWER, result));
3717  ensure(le(xmbr_id, result));
3718 
3719  // Exit
3720 
3721  return;
3722 }
3723 
3724 void
3727 {
3728 
3729  // Preconditions:
3730 
3731  require(xjem1 != TOP_INDEX);
3732  require(xjem1 != BOTTOM_INDEX);
3733  require(cover_is_empty(LOWER, xjem1));
3734  require(cover_is_empty(UPPER, xjem1));
3735 
3736  // Body:
3737 
3738  // Make xjem1 the greatest jem of xjem2
3739 
3740  // We want to put xjem1 on top of the current greatest jem of xjem2,
3741  // unless the current greatest jem is the top. The top must always
3742  // be the top, so if the current greatest jem is the top, we'll
3743  // put the new jem immediately under it. Either way, we first find
3744  // the current greatest jem.
3745 
3746  pod_index_type lgjem = greatest_jem(xjem2);
3747 
3748  if(lgjem != TOP_INDEX)
3749  {
3750  // Current greatest jem is not the top;
3751  // Put new member on top of it.
3752 
3753  transfer_cover(lgjem, xjem1, false);
3754  new_link(xjem1, lgjem);
3755  }
3756  else
3757  {
3758  // Other member is the top;
3759  // Put new member directly under it.
3760 
3761  transfer_cover(lgjem, xjem1, true);
3762  new_link(lgjem, xjem1);
3763  }
3764 
3765  // Postconditions:
3766 
3767  ensure(is_jem(xjem2, xjem1));
3768  ensure(greatest_jem(xjem2) != TOP_INDEX ?
3769  greatest_jem(xjem2) == xjem1 :
3770  true );
3771 
3772  // Exit
3773 
3774  return;
3775 }
3776 
3777 void
3779 link_greatest_jem(const scoped_index& xjem1, const scoped_index& xjem2)
3780 {
3781 
3782  // Preconditions:
3783 
3784  require(xjem1 != TOP_INDEX);
3785  require(xjem1 != BOTTOM_INDEX);
3786  require(cover_is_empty(LOWER, xjem1));
3787  require(cover_is_empty(UPPER, xjem1));
3788 
3789  // Body:
3790 
3791  link_greatest_jem(xjem1.hub_pod(), xjem2.hub_pod());
3792 
3793  // Postconditions:
3794 
3795  ensure(is_jem(xjem2, xjem1));
3796  ensure(greatest_jem(xjem2.hub_pod()) != TOP_INDEX ?
3797  greatest_jem(xjem2.hub_pod()) == xjem1.hub_pod() :
3798  true );
3799 
3800  // Exit
3801 
3802  return;
3803 }
3804 
3805 void
3808 {
3809  // Preconditions:
3810 
3811  require(xjem1 != TOP_INDEX);
3812  require(xjem1 != BOTTOM_INDEX);
3813  require(cover_is_empty(LOWER, xjem1));
3814  require(cover_is_empty(UPPER, xjem1));
3815 
3816  // Body:
3817 
3818  // Make xjem1 the least jem of xjem2
3819 
3820  // We want to put xjem1 directly below the current least jem of xjem2,
3821  // unless the current least jem is the bottom. The bottom must always
3822  // be the bottom, so if the current least jem is the bottom, we'll
3823  // put the new jem immediately above it. Either way, we first find
3824  // the current least jem.
3825 
3826  pod_index_type lljem = least_jem(xjem2);
3827 
3828  if(is_jim(lljem) || lljem == BOTTOM_INDEX)
3829  {
3830  // the current least jem is a jim or is the bottom;
3831  // Put new member directly on top of it.
3832 
3833  transfer_cover(lljem, xjem1, false);
3834  new_link(xjem1, lljem);
3835  }
3836  else
3837  {
3838  // Current least jem is a jrm and not the bottom;
3839  // Put new member below it.
3840 
3841  transfer_cover(lljem, xjem1, true);
3842  new_link(lljem, xjem1);
3843  }
3844 
3845  // Postconditions:
3846 
3847  ensure(is_jem(xjem2, xjem1));
3848  ensure((least_jem(xjem2) == xjem1) ||
3849  is_jim(least_jem(xjem2)) ||
3850  (least_jem(xjem2) == BOTTOM_INDEX));
3851 
3852  // Exit
3853 
3854  return;
3855 }
3856 
3857 void
3859 link_least_jem(const scoped_index& xjem1, const scoped_index& xjem2)
3860 {
3861  // Preconditions:
3862 
3863  require(xjem1 != TOP_INDEX);
3864  require(xjem1 != BOTTOM_INDEX);
3865  require(cover_is_empty(LOWER, xjem1));
3866  require(cover_is_empty(UPPER, xjem1));
3867 
3868  // Body:
3869 
3870  link_least_jem(xjem1.hub_pod(), xjem2.hub_pod());
3871 
3872  // Postconditions:
3873 
3874  ensure(is_jem(xjem2, xjem1));
3875  ensure((least_jem(xjem2.hub_pod()) == xjem1.hub_pod()) ||
3876  is_jim(least_jem(xjem2.hub_pod())) ||
3877  (least_jem(xjem2.hub_pod()) == BOTTOM_INDEX));
3878 
3879  // Exit
3880 
3881  return;
3882 }
3883 
3884 void
3887 {
3888  // Preconditions:
3889 
3890  require(xjem1 != xjem2);
3891  require(!is_jem(xjem1, BOTTOM_INDEX));
3892  require(state_is_read_write_accessible());
3893  require(contains_member(xjem1, false));
3894  require(contains_member(xjem2, false));
3895  require(!is_jim(xjem1));
3896  require(!is_jim(xjem2));
3897  require(cover_is_equal(LOWER, xjem1, xjem2));
3898 
3899  // Body:
3900 
3901  // link join-equivalence class of xjem2
3902  // linearly below the least jem of xjem1
3903 
3904  // get the least and greatest members of both equivalence classes
3905 
3906  pod_index_type gjem1 = greatest_jem(xjem1);
3907  pod_index_type gjem2 = greatest_jem(xjem2);
3908 
3909  pod_index_type ljem1 = least_jem(xjem1);
3910  pod_index_type ljem2 = least_jem(xjem2);
3911 
3912  if(gjem1 != gjem2)
3913  {
3914  // Transfer the upper cover of gjem2 to gjem1.
3915 
3916  transfer_cover(gjem2, gjem1, false);
3917  }
3918 
3919 
3920  if(ljem1 != ljem2)
3921  {
3922  // Transfer the lower cover of ljem1 to ljem2.
3923 
3924  transfer_cover(ljem1, ljem2, true);
3925  }
3926 
3927 
3928  if(ljem1 != gjem2)
3929  {
3930  // Cover gjem2 with ljem1.
3931 
3932  new_link(ljem1, gjem2);
3933  }
3934 
3935  // Postconditions:
3936 
3937  ensure(le(xjem1, xjem2));
3938 
3939  // Exit
3940 
3941  return;
3942 }
3943 
3944 void
3946 merge_jems(const scoped_index& xjem1, const scoped_index& xjem2)
3947 {
3948  // Preconditions:
3949 
3950  require(xjem1 !=~ xjem2);
3951  require(!is_jem(xjem1, bottom().index()));
3952  require(state_is_read_write_accessible());
3953  require(contains_member(xjem1, false));
3954  require(contains_member(xjem2, false));
3955  require(!is_jim(xjem1));
3956  require(!is_jim(xjem2));
3957  require(cover_is_equal(LOWER, xjem1, xjem2));
3958 
3959  // Body:
3960 
3961  merge_jems(xjem1.hub_pod(), xjem2.hub_pod());
3962 
3963  // Postconditions:
3964 
3965  ensure(le(xjem1, xjem2));
3966 
3967  // Exit
3968 
3969  return;
3970 }
3971 
3972 // PROTECTED FUNCTIONS
3973 
3974 // PRIVATE FUNCTIONS
3975 
3976 
3977 // ===========================================================
3978 // COVER RELATION FACET
3979 // ===========================================================
3980 
3981 // PUBLIC FUNCTIONS
3982 
3983 void
3986 {
3987 
3988  // Preconditions:
3989 
3990  require(contains_member(xgreater, false));
3991  require(xgreater != BOTTOM_INDEX);
3992  require(contains_member(xlesser, false));
3993  require(xlesser != TOP_INDEX);
3994 
3995  // Body:
3996 
3997  // Make some useful local variables
3998 
3999  crg().insert_cover_member(xgreater, UPPER, xlesser);
4000  crg().insert_cover_member(xlesser, LOWER, xgreater);
4001 
4002  // Postconditions:
4003 
4008 
4009  ensure(unexecutable(contains_link(xgreater, xlesser)));
4010 
4011  // Exit:
4012 
4013  return;
4014 }
4015 
4016 void
4018 new_link(const scoped_index& xgreater, const scoped_index& xlesser)
4019 {
4020 
4021  // Preconditions:
4022 
4023  require(contains_member(xgreater, false));
4024  require(xgreater.hub_pod() != BOTTOM_INDEX);
4025  require(contains_member(xlesser, false));
4026  require(xlesser.hub_pod() != TOP_INDEX);
4027 
4028  // Body:
4029 
4030  new_link(xgreater.hub_pod(), xlesser.hub_pod());
4031 
4032  // Postconditions:
4033 
4038 
4039  ensure(unexecutable(contains_link(xgreater, xlesser)));
4040 
4041  // Exit:
4042 
4043  return;
4044 
4045 }
4046 
4047 void
4050 {
4051 
4052  // Preconditions:
4053 
4054  require(state_is_read_write_accessible());
4055 
4056  // Body:
4057 
4058  crg().remove_cover_member(xgreater, UPPER, xlesser);
4059  crg().remove_cover_member(xlesser, LOWER, xgreater);
4060 
4061  // Postconditions:
4062 
4063  ensure(invariant());
4064  ensure(!contains_link(xgreater, xlesser));
4065 
4066  // Exit:
4067 
4068  return;
4069 }
4070 
4071 void
4073 delete_link(const scoped_index& xgreater, const scoped_index& xlesser)
4074 {
4075 
4076  // Preconditions:
4077 
4078  require(state_is_read_write_accessible());
4079 
4080  // Body:
4081 
4082  delete_link(xgreater.hub_pod(), xlesser.hub_pod());
4083 
4084  // Postconditions:
4085 
4086  ensure(invariant());
4087  ensure(!contains_link(xgreater, xlesser));
4088 
4089  // Exit:
4090 
4091  return;
4092 }
4093 
4094 bool
4097 {
4098  bool result = false;
4099 
4100  // Preconditions:
4101 
4102  require(state_is_read_accessible());
4103  require(contains_member(xlesser, false));
4104  require(contains_member(xgreater, false));
4105 
4106  // Body:
4107 
4108  result =
4109  crg().cover_contains_member(LOWER, xgreater, xlesser) &&
4110  crg().cover_contains_member(UPPER, xlesser, xgreater);
4111 
4112  // Postconditions:
4113 
4114  // Exit
4115 
4116  return result;
4117 }
4118 
4119 bool
4121 contains_link(const scoped_index& xgreater, const scoped_index& xlesser) const
4122 {
4123  bool result = false;
4124 
4125  // Preconditions:
4126 
4127  require(state_is_read_accessible());
4128  require(contains_member(xlesser, false));
4129  require(contains_member(xgreater, false));
4130 
4131  // Body:
4132 
4133  return contains_link(xgreater.hub_pod(), xlesser.hub_pod());
4134 }
4135 
4138 cover_id_space_id(bool xlower, pod_index_type xmbr_hub_id) const
4139 {
4140  // Preconditions:
4141 
4142  require(contains_member(xmbr_hub_id));
4143 
4144  // Body:
4145 
4146  pod_index_type result = crg().cover_id_space_id(xlower, xmbr_hub_id);
4147 
4148  // Postconditions:
4149 
4150  ensure(is_valid(result));
4151 
4152  // Exit:
4153 
4154  return result;
4155 }
4156 
4159 cover_id_space_id(bool xlower, const scoped_index& xmbr_id) const
4160 {
4161  // Preconditions:
4162 
4163  require(contains_member(xmbr_id));
4164 
4165  // Body:
4166 
4167  pod_index_type result = cover_id_space_id(xlower, xmbr_id.hub_pod());
4168 
4169  // Postconditions:
4170 
4171  ensure(is_valid(result));
4172 
4173  // Exit:
4174 
4175  return result;
4176 }
4177 
4180 get_cover_id_space(bool xlower, pod_index_type xmbr_hub_id) const
4181 {
4182  // Preconditions:
4183 
4184  require(state_is_read_accessible());
4185  require(contains_member(xmbr_hub_id, false));
4186 
4187  // Body:
4188 
4189  return crg().get_cover_id_space(xlower, xmbr_hub_id);
4190 }
4191 
4194 get_cover_id_space(bool xlower, const scoped_index& xmbr_id) const
4195 {
4196  // Preconditions:
4197 
4198  require(state_is_read_accessible());
4199  require(contains_member(xmbr_id));
4200 
4201  // Body:
4202 
4203  return get_cover_id_space(xlower, xmbr_id.hub_pod());
4204 }
4205 
4206 void
4209 {
4210  // Preconditions:
4211 
4212  require(state_is_read_accessible());
4213 
4214  // Body:
4215 
4216  crg().release_cover_id_space(xcover_id_space);
4217 
4218  // Postconditions:
4219 
4220  ensure(!xcover_id_space.is_attached());
4221 
4222  // Exit:
4223 
4224  return;
4225 }
4226 
4229 get_cover_id_space_iterator(bool xlower, pod_index_type xmbr_hub_id) const
4230 {
4231  // Preconditions:
4232 
4233  require(state_is_read_accessible());
4234  require(contains_member(xmbr_hub_id, false));
4235 
4236  // Body:
4237 
4238  return crg().get_cover_id_space_iterator(xlower, xmbr_hub_id);
4239 }
4240 
4243 get_cover_id_space_iterator(bool xlower, const scoped_index& xmbr_id) const
4244 {
4245  // Preconditions:
4246 
4247  require(state_is_read_accessible());
4248  require(contains_member(xmbr_id));
4249 
4250  // Body:
4251 
4252  return get_cover_id_space_iterator(xlower, xmbr_id.hub_pod());
4253 }
4254 
4255 void
4258 {
4259  // Preconditions:
4260 
4261  require(state_is_read_accessible());
4262 
4263  // Body:
4264 
4265  crg().release_cover_id_space_iterator(xcover_itr);
4266 
4267  // Postconditions:
4268 
4269  ensure(!xcover_itr.is_attached());
4270 
4271  // Exit:
4272 
4273  return;
4274 }
4275 
4276 bool
4279  pod_index_type xmbr_hub_id,
4280  const index_space_iterator& xitr) const
4281 {
4282  // Preconditions:
4283 
4284  require(state_is_read_accessible());
4285  require(contains_member(xmbr_hub_id, false));
4286 
4287  // Body:
4288 
4289  return crg().cover_contains_iterator(xlower, xmbr_hub_id, xitr);
4290 }
4291 
4292 bool
4295  const scoped_index& xmbr_id,
4296  const index_space_iterator& xitr) const
4297 {
4298  // Preconditions:
4299 
4300  require(state_is_read_accessible());
4301  require(contains_member(xmbr_id));
4302 
4303  // Body:
4304 
4305  return cover_contains_iterator(xlower, xmbr_id.hub_pod(), xitr);
4306 }
4307 
4308 bool
4310 cover_is_empty(bool xlower, pod_index_type xmbr_hub_id) const
4311 {
4312  // Preconditions:
4313 
4314  require(state_is_read_accessible());
4315  require(contains_member(xmbr_hub_id, false));
4316 
4317  // Body:
4318 
4319  return crg().cover_is_empty(xlower, xmbr_hub_id);
4320 }
4321 
4322 bool
4324 cover_is_empty(bool xlower, const scoped_index& xmbr_id) const
4325 {
4326  // Preconditions:
4327 
4328  require(state_is_read_accessible());
4329  require(contains_member(xmbr_id, false));
4330 
4331  // Body:
4332 
4333  return cover_is_empty(xlower, xmbr_id.hub_pod());
4334 }
4335 
4336 bool
4338 cover_is_singleton(bool xlower, pod_index_type xmbr_hub_id) const
4339 {
4340  // Preconditions:
4341 
4342  require(state_is_read_accessible());
4343  require(contains_member(xmbr_hub_id, false));
4344 
4345  // Body:
4346 
4347  return crg().cover_is_singleton(xlower, xmbr_hub_id);
4348 }
4349 
4350 bool
4352 cover_is_singleton(bool xlower, const scoped_index& xmbr_id) const
4353 {
4354  // Preconditions:
4355 
4356  require(state_is_read_accessible());
4357  require(contains_member(xmbr_id, false));
4358 
4359  // Body:
4360 
4361  return cover_is_singleton(xlower, xmbr_id.hub_pod());
4362 }
4363 
4366 cover_ct(bool xlower, pod_index_type xmbr_hub_id) const
4367 {
4368  int result;
4369 
4370  // Preconditions:
4371 
4372  require(state_is_read_accessible());
4373  require(contains_member(xmbr_hub_id, false));
4374 
4375  // Body:
4376 
4377  result = crg().cover_ct(xlower, xmbr_hub_id);
4378 
4379  // Postconditions:
4380 
4381  ensure(result >= 0);
4382 
4383  // Exit
4384 
4385  return result;
4386 }
4387 
4390 cover_ct(bool xlower, const scoped_index& xmbr_id) const
4391 {
4392  int result;
4393 
4394  // Preconditions:
4395 
4396  require(state_is_read_accessible());
4397  require(contains_member(xmbr_id, false));
4398 
4399  // Body:
4400 
4401  result = cover_ct(xlower, xmbr_id.hub_pod());
4402 
4403  // Postconditions:
4404 
4405  ensure(result >= 0);
4406 
4407  // Exit
4408 
4409  return result;
4410 }
4411 
4412 bool
4415  pod_index_type xmbr_hub_id,
4416  pod_index_type xother_mbr_hub_id) const
4417 {
4418  // Preconditions:
4419 
4420  require(state_is_read_accessible());
4421  require(contains_member(xmbr_hub_id, false));
4422 
4423  // Body:
4424 
4425  return crg().cover_contains_member(xlower, xmbr_hub_id, xother_mbr_hub_id);
4426 }
4427 
4428 bool
4431  const scoped_index& xmbr_id,
4432  const scoped_index& xother_mbr_id) const
4433 {
4434  // Preconditions:
4435 
4436  require(state_is_read_accessible());
4437  require(contains_member(xmbr_id));
4438 
4439  // Body:
4440 
4441  return cover_contains_member(xlower,
4442  xmbr_id.hub_pod(),
4443  xother_mbr_id.hub_pod());
4444 }
4445 
4446 bool
4448 cover_is_equal(bool xlower,
4449  pod_index_type xmbr_hub_id,
4450  pod_index_type xother_mbr_hub_id) const
4451 {
4452  // Preconditions:
4453 
4454  require(state_is_read_accessible());
4455  require(contains_member(xmbr_hub_id, false));
4456  require(contains_member(xother_mbr_hub_id, false));
4457 
4458  // Body:
4459 
4460  return crg().cover_is_equal(xlower, xmbr_hub_id, xother_mbr_hub_id);
4461 }
4462 
4463 bool
4465 cover_is_equal(bool xlower,
4466  const scoped_index& xmbr_id,
4467  const scoped_index& xother_mbr_id) const
4468 {
4469  // Preconditions:
4470 
4471  require(state_is_read_accessible());
4472  require(contains_member(xmbr_id));
4473  require(contains_member(xother_mbr_id));
4474 
4475  // Body:
4476 
4477  return cover_is_equal(xlower,
4478  xmbr_id.hub_pod(),
4479  xother_mbr_id.hub_pod());
4480 }
4481 
4484 first_cover_member(bool xlower, pod_index_type xmbr_hub_id) const
4485 {
4486  // Preconditions:
4487 
4488  require(state_is_read_accessible());
4489  require(contains_member(xmbr_hub_id, false));
4490  require(!cover_is_empty(xlower, xmbr_hub_id));
4491 
4492  // Body:
4493 
4494  return crg().first_cover_member(xlower, xmbr_hub_id);
4495 }
4496 
4497 void
4499 first_cover_member(bool xlower, const scoped_index& xmbr_id,
4500  scoped_index& result) const
4501 {
4502  // Preconditions:
4503 
4504  require(state_is_read_accessible());
4505  require(contains_member(xmbr_id));
4506  require(!cover_is_empty(xlower, xmbr_id));
4507 
4508  // Body:
4509 
4510  result.put(member_hub_id_space(false),
4511  first_cover_member(xlower, xmbr_id.hub_pod()));
4512 
4513  // Postconditions:
4514 
4515  // Exit:
4516 
4517  return;
4518 }
4519 
4520 void
4523  bool xlower,
4524  pod_index_type xmbr_hub_id)
4525 {
4526  // Preconditions:
4527 
4528  require(state_is_read_write_accessible());
4529  require(contains_member(xmbr_hub_id, false));
4530  require(!cover_contains_member(xlower, xmbr_hub_id, xother_mbr_hub_id));
4531 
4532  // Body:
4533 
4534  crg().insert_cover_member(xother_mbr_hub_id, xlower, xmbr_hub_id);
4535 
4536  // Postconditions:
4537 
4538  // Unexecutable because average performance is O(cover_ct)
4539 
4540  ensure(unexecutable(cover_contains_member(xlower, xmbr_hub_id, xother_mbr_hub_id)));
4541 
4542  // Exit:
4543 
4544  return;
4545 }
4546 
4547 void
4549 insert_cover_member(const scoped_index& xother_mbr_id,
4550  bool xlower,
4551  const scoped_index& xmbr_id)
4552 {
4553  // Preconditions:
4554 
4555  require(state_is_read_write_accessible());
4556  require(contains_member(xmbr_id));
4557 
4558  // Body:
4559 
4560  insert_cover_member(xother_mbr_id.hub_pod(),
4561  xlower,
4562  xmbr_id.hub_pod());
4563 
4564  // Postconditions:
4565 
4566  // Unexecutable because average performance is O(cover_ct)
4567 
4568  ensure(unexecutable(cover_contains_member(xlower, xmbr_id, xother_mbr_id)));
4569 
4570  // Exit:
4571 
4572  return;
4573 }
4574 
4575 void
4578  bool xlower,
4579  pod_index_type xmbr_hub_id,
4580  index_space_iterator& xitr)
4581 {
4582  // Preconditions:
4583 
4584  require(state_is_read_write_accessible());
4585  require(contains_member(xmbr_hub_id, false));
4586  require(cover_contains_iterator(xlower, xmbr_hub_id, xitr));
4587 
4588  // Body:
4589 
4590  crg().insert_cover_member(xother_mbr_hub_id, xlower, xmbr_hub_id, xitr);
4591 
4592  // Postconditions:
4593 
4594  // Unexecutable because average performance is O(cover_ct)
4595 
4596  ensure(unexecutable(cover_contains_member(xlower, xmbr_hub_id, xother_mbr_hub_id)));
4597 
4598  // Exit:
4599 
4600  return;
4601 }
4602 
4603 void
4605 insert_cover_member(const scoped_index& xother_mbr_id,
4606  bool xlower,
4607  const scoped_index& xmbr_id,
4608  index_space_iterator& xitr)
4609 {
4610  // Preconditions:
4611 
4612  require(state_is_read_write_accessible());
4613  require(contains_member(xmbr_id));
4614  require(cover_contains_iterator(xlower, xmbr_id, xitr));
4615 
4616  // Body:
4617 
4618  insert_cover_member(xother_mbr_id.hub_pod(),
4619  xlower,
4620  xmbr_id.hub_pod(),
4621  xitr);
4622 
4623  // Postconditions:
4624 
4625  // Unexecutable because average performance is O(cover_ct)
4626 
4627  ensure(unexecutable(cover_contains_member(xlower, xmbr_id, xother_mbr_id)));
4628 
4629  // Exit:
4630 
4631  return;
4632 }
4633 
4634 void
4637  bool xlower,
4638  pod_index_type xmbr_hub_id)
4639 {
4640  // Preconditions:
4641 
4642  require(state_is_read_write_accessible());
4643  require(contains_member(xmbr_hub_id, false));
4644 
4645  // Body:
4646 
4647  crg().remove_cover_member(xother_mbr_hub_id, xlower, xmbr_hub_id);
4648 
4649  // Postconditions:
4650 
4651  // Unexecutable because average performance is O(cover_ct)
4652 
4653  ensure(unexecutable(!cover_contains_member(xlower, xmbr_hub_id, xother_mbr_hub_id)));
4654 
4655  // Exit:
4656 
4657  return;
4658 }
4659 
4660 void
4662 remove_cover_member(const scoped_index& xother_mbr_id,
4663  bool xlower,
4664  const scoped_index& xmbr_id)
4665 {
4666  // Preconditions:
4667 
4668  require(state_is_read_write_accessible());
4669  require(contains_member(xmbr_id));
4670 
4671  // Body:
4672 
4673  remove_cover_member(xother_mbr_id.hub_pod(),
4674  xlower,
4675  xmbr_id.hub_pod());
4676 
4677  // Postconditions:
4678 
4679  // Unexecutable because average performance is O(cover_ct)
4680 
4681  ensure(unexecutable(!cover_contains_member(xlower, xmbr_id, xother_mbr_id)));
4682 
4683  // Exit:
4684 
4685  return;
4686 }
4687 
4688 void
4691  bool xlower,
4692  pod_index_type xmbr_hub_id)
4693 {
4694  // Preconditions:
4695 
4696  require(state_is_read_write_accessible());
4697  require(contains_member(xmbr_hub_id, false));
4698 
4699  // Body:
4700 
4701  crg().remove_cover_member(xitr, xlower, xmbr_hub_id);
4702 
4703  // Postconditions:
4704 
4705  // Unexecutable because average performance is O(cover_ct)
4706 
4707  ensure(unexecutable(!cover_contains_member(xlower, xmbr_hub_id, old_xitr_item)));
4708 
4709  // Exit:
4710 
4711  return;
4712 }
4713 
4714 void
4717  bool xlower,
4718  const scoped_index& xmbr_id)
4719 {
4720  // Preconditions:
4721 
4722  require(state_is_read_write_accessible());
4723  require(contains_member(xmbr_id));
4724 
4725  // Body:
4726 
4727  remove_cover_member(xitr, xlower, xmbr_id.hub_pod());
4728 
4729  // Postconditions:
4730 
4731  // Unexecutable because average performance is O(cover_ct)
4732 
4733  ensure(unexecutable(!cover_contains_member(xlower, xmbr_id, old_xitr_item)));
4734 
4735  // Exit:
4736 
4737  return;
4738 }
4739 
4740 void
4742 replace_cover_member(pod_index_type xold_other_mbr_hub_id,
4743  pod_index_type xnew_other_mbr_hub_id,
4744  bool xlower,
4745  pod_index_type xmbr_hub_id)
4746 {
4747  // Preconditions:
4748 
4749  require(state_is_read_write_accessible());
4750  require(contains_member(xmbr_hub_id, false));
4751 
4752  define_old_variable(bool old_cover_contains_old_other_mbr_hub_id = cover_contains_member(xlower, xmbr_hub_id, xold_other_mbr_hub_id));
4753 
4754  // Body:
4755 
4756  crg().replace_cover_member(xold_other_mbr_hub_id, xnew_other_mbr_hub_id, xlower, xmbr_hub_id);
4757 
4758  // Postconditions:
4759 
4760  // Unexecutable because average performance is O(cover_ct)
4761 
4762  ensure(unexecutable(!cover_contains_member(xlower, xmbr_hub_id, xold_other_mbr_hub_id)));
4763  ensure(unexecutable(old_cover_contains_old_other_mbr_hub_id ? cover_contains_member(xlower, xmbr_hub_id, xnew_other_mbr_hub_id) : true));
4764 
4765  // Exit:
4766 
4767  return;
4768 }
4769 
4770 void
4772 replace_cover_member(const scoped_index& xold_other_mbr_id,
4773  const scoped_index& xnew_other_mbr_id,
4774  bool xlower,
4775  const scoped_index& xmbr_id)
4776 {
4777  // Preconditions:
4778 
4779  require(state_is_read_write_accessible());
4780  require(contains_member(xmbr_id));
4781 
4782  define_old_variable(bool old_cover_contains_old_other_mbr_id = cover_contains_member(xlower, xmbr_id, xold_other_mbr_id));
4783 
4784  // Body:
4785 
4786  replace_cover_member(xold_other_mbr_id.hub_pod(),
4787  xnew_other_mbr_id.hub_pod(),
4788  xlower,
4789  xmbr_id.hub_pod());
4790 
4791  // Postconditions:
4792 
4793  // Unexecutable because average performance is O(cover_ct)
4794 
4795  ensure(unexecutable(!cover_contains_member(xlower, xmbr_id, xold_other_mbr_id)));
4796  ensure(unexecutable(old_cover_contains_old_other_mbr_id ? cover_contains_member(xlower, xmbr_id, xnew_other_mbr_id) : true));
4797 
4798  // Exit:
4799 
4800  return;
4801 }
4802 
4803 void
4805 clear_cover(bool xlower, pod_index_type xmbr_hub_id)
4806 {
4807  // Preconditions:
4808 
4809  require(state_is_read_write_accessible());
4810  require(contains_member(xmbr_hub_id, false));
4811 
4812  // Body:
4813 
4814  crg().clear_cover(xlower, xmbr_hub_id);
4815 
4816  // Postconditions:
4817 
4818  ensure(cover_is_empty(xlower, xmbr_hub_id));
4819 
4820  // Exit:
4821 
4822  return;
4823 }
4824 
4825 void
4827 clear_cover(bool xlower, const scoped_index& xmbr_id)
4828 {
4829  // Preconditions:
4830 
4831  require(state_is_read_write_accessible());
4832  require(contains_member(xmbr_id));
4833 
4834  // Body:
4835 
4836  clear_cover(xlower, xmbr_id.hub_pod());
4837 
4838  // Postconditions:
4839 
4840  ensure(cover_is_empty(xlower, xmbr_id));
4841 
4842  // Exit:
4843 
4844  return;
4845 }
4846 
4847 void
4849 copy_cover(bool xlower, pod_index_type xmbr_hub_id, pod_index_type xother_mbr_hub_id)
4850 {
4851  // Preconditions:
4852 
4853  require(state_is_read_write_accessible());
4854  require(contains_member(xmbr_hub_id, false));
4855  require(contains_member(xother_mbr_hub_id, false));
4856 
4857  // Body::
4858 
4859  crg().copy_cover(xlower, xmbr_hub_id, xother_mbr_hub_id);
4860 
4861  // Postconditions:
4862 
4863  // Unexecutable because average performance is O(cover_ct)
4864 
4865  ensure(unexecutable(cover_is_equal(xlower, xmbr_hub_id, xother_mbr_hub_id)));
4866 
4867  // Exit:
4868 
4869  return;
4870 }
4871 
4872 void
4874 copy_cover(bool xlower, const scoped_index& xmbr_id, const scoped_index& xother_mbr_id)
4875 {
4876  // Preconditions:
4877 
4878  require(state_is_read_write_accessible());
4879  require(contains_member(xmbr_id));
4880  require(contains_member(xother_mbr_id));
4881 
4882  // Body::
4883 
4884  copy_cover(xlower,
4885  xmbr_id.hub_pod(),
4886  xother_mbr_id.hub_pod());
4887 
4888  // Postconditions:
4889 
4890  // Unexecutable because average performance is O(cover_ct)
4891 
4892  ensure(unexecutable(cover_is_equal(xlower, xmbr_id, xother_mbr_id)));
4893 
4894  // Exit:
4895 
4896  return;
4897 }
4898 
4899 void
4902  pod_index_type xmbr_hub_end)
4903 {
4904  // Preconditions:
4905 
4906  require(state_is_read_write_accessible());
4907  require_for_range(pod_index_type i=xmbr_hub_begin, i<xmbr_hub_end, ++i, contains_member(i));
4908 
4909  // Body:
4910 
4911  crg().append_upper_cover_of_bottom(xmbr_hub_begin, xmbr_hub_end);
4912 
4913  // Postconditions:
4914 
4915  ensure_for_range(pod_index_type i=xmbr_hub_begin, i<xmbr_hub_end, ++i, cover_contains_member(UPPER, BOTTOM_INDEX, i));
4916 
4917  // Exit:
4918 
4919  return;
4920 }
4921 
4922 void
4925  const scoped_index& xmbr_end)
4926 {
4927  // Preconditions:
4928 
4929  require(state_is_read_write_accessible());
4930  require_for_range(scoped_index i=xmbr_begin, i<xmbr_end, ++i, contains_member(i));
4931 
4932  // Body::
4933 
4934  append_upper_cover_of_bottom(xmbr_begin.hub_pod(), xmbr_end.hub_pod());
4935 
4936  // Postconditions:
4937 
4938  ensure_for_range(scoped_index i=xmbr_begin, i<xmbr_end, ++i, cover_contains_member(UPPER, BOTTOM_INDEX, i.hub_pod()));
4939 
4940  // Exit:
4941 
4942  return;
4943 }
4944 
4945 // PROTECTED FUNCTIONS
4946 
4947 void
4950 {
4951  // Preconditions:
4952 
4953  require(contains_member(xsrc));
4954  require(contains_member(xdst));
4955 
4956  // Body:
4957 
4958  index_space_iterator& src_itr = get_cover_id_space_iterator(xlower, xsrc);
4959  while(!src_itr.is_done())
4960  {
4961  // Remove src index from the opposing cover of
4962  // the current member of src's xlower cover.
4963 
4964  // Could use delete_link if we were careful not to screw up
4965  // the iterator, but this method is a little faster since it
4966  // involves only half as many finds.
4967 
4968  // Note that "opposing cover" means the complement of xlower
4969  // is passed to remve_cover_member.
4970 
4971  remove_cover_member(xsrc, !xlower, src_itr.hub_pod());
4972 
4973  // Insert a link from dst to the current member of src's cover.
4974 
4975  xlower ? new_link(xdst, src_itr.hub_pod()) : new_link(src_itr.hub_pod(), xdst);
4976 
4977  // Move on.
4978 
4979  src_itr.next();
4980  }
4981  release_cover_id_space_iterator(src_itr);
4982 
4983  // Now we can just erase src's cover
4984 
4985  clear_cover(xlower, xsrc);
4986 
4987 
4988  // Postconditions:
4989 
4990  // Exit
4991 
4992  return;
4993 }
4994 
4995 // PRIVATE FUNCTIONS
4996 
4997 
4998 // ===========================================================
4999 // POWERSET FACET
5000 // ===========================================================
5001 
5002 // PUBLIC FUNCTIONS
5003 
5007 {
5008 
5009  // Preconditions:
5010 
5011  require(state_is_read_accessible());
5012 
5013  // Body:
5014 
5015  size_type result = powerset().subposet_ct();
5016 
5017  // Postconditions:
5018 
5019  ensure(result >= 0);
5020 
5021  return result;
5022 }
5023 
5024 int
5027 {
5028  int result;
5029 
5030  // Preconditions:
5031 
5032  require(state_is_read_accessible());
5033 
5034  // Body:
5035 
5036  result = powerset().standard_subposet_ct();
5037 
5038  // Postconditions:
5039 
5040  ensure(result >= 0);
5041 
5042  return result;
5043 }
5044 
5045 bool
5048 {
5049  bool result;
5050 
5051  // Preconditions:
5052 
5053  require(state_is_read_accessible());
5054 
5055  // Body:
5056 
5057  result = (subposet_ct() == standard_subposet_ct());
5058 
5059  // Postconditions:
5060 
5061  ensure(result == (subposet_ct() == standard_subposet_ct()));
5062 
5063  return result;
5064 }
5065 
5069 {
5070 
5071  // Preconditions:
5072 
5073  require(state_is_read_accessible());
5074 
5075  // Body:
5076 
5077  scoped_index result = powerset().subposet_index_ub();
5078 
5079  // Postconditions:
5080 
5081  ensure(result.is_positive());
5082 
5083  return result;
5084 }
5085 
5088 subposet_id(const std::string& xname) const
5089 {
5090  // Preconditions:
5091 
5092  require(state_is_read_accessible());
5093  require(!xname.empty());
5094 
5095  // Body:
5096 
5097  pod_index_type result = powerset().subposet_name_map().index(xname);
5098 
5099  // Postconditions:
5100 
5101  ensure(invariant());
5102  ensure(is_valid(result) ? includes_subposet(result) : true);
5103 
5104  // Exit
5105 
5106  return result;
5107 }
5108 
5109 void
5111 subposet_id(const std::string& xname, scoped_index& result) const
5112 {
5113  // Preconditions:
5114 
5115  require(state_is_read_accessible());
5116  require(!xname.empty());
5117 
5118  // Body:
5119 
5120  result = powerset().hub_id(powerset().subposet_name_map().index(xname));
5121 
5122  // Postconditions:
5123 
5124  ensure(invariant());
5125  ensure(result.is_valid() ? includes_subposet(result) : true);
5126 
5127  // Exit
5128 
5129  return;
5130 }
5131 
5135 {
5136  // Preconditions:
5137 
5138  require(state_is_read_accessible());
5139 
5140  // Body:
5141 
5142  return powerset().get_subposet_id_space_iterator();
5143 }
5144 
5145 void
5148 {
5149  // Preconditions:
5150 
5151  require(state_is_read_accessible());
5152 
5153  // Body:
5154 
5155  powerset().release_subposet_id_space_iterator(xitr);
5156 
5157  // Postconditions:
5158 
5159  // Exit:
5160 
5161  return;
5162 }
5163 
5164 bool
5166 includes_subposet(pod_index_type xsubposet_hub_id, bool xauto_access) const
5167 {
5168  bool result;
5169 
5170  // Preconditions:
5171 
5172  require(state_is_auto_read_accessible(xauto_access));
5173 
5174  // Body:
5175 
5176  if(xauto_access)
5177  {
5178  get_read_access();
5179  }
5180 
5181  result = powerset().contains_subposet(xsubposet_hub_id);
5182 
5183  if(xauto_access)
5184  {
5185  release_access();
5186  }
5187 
5188  // Postconditions:
5189 
5190  // Exit
5191 
5192  return result;
5193 }
5194 
5195 bool
5197 includes_subposet(const scoped_index& xsubposet_id, bool xauto_access) const
5198 {
5199  bool result;
5200 
5201  // Preconditions:
5202 
5203  require(xauto_access || state_is_read_accessible());
5204 
5205  // Body:
5206 
5207  return includes_subposet(xsubposet_id.hub_pod(), xauto_access);
5208 }
5209 
5210 bool
5212 includes_subposet(const std::string& xname, bool xauto_access) const
5213 {
5214  bool result;
5215 
5216  // Preconditions:
5217 
5218  require(state_is_auto_read_accessible(xauto_access));
5219 
5220  // Body:
5221 
5222  if(xauto_access)
5223  {
5224  get_read_access();
5225  }
5226 
5227  pod_index_type lid = subposet_id(xname);
5228  result = is_valid(lid) ? includes_subposet(lid, false) : false;
5229 
5230  if(xauto_access)
5231  {
5232  release_access();
5233  }
5234 
5235  // Postconditions:
5236 
5237  // Exit
5238 
5239  return result;
5240 }
5241 
5242 bool
5244 includes_subposet(const subposet* xs, bool xauto_access) const
5245 {
5246  bool result;
5247 
5248  // Preconditions:
5249 
5250  require(!xauto_access ? state_is_read_accessible() : true);
5251 
5252  // Body:
5253 
5254  result = xs->is_attached() &&
5255  xs->host()->is_same_state(this) &&
5256  includes_subposet(xs->index(), xauto_access);
5257 
5258  // Postconditions:
5259 
5260  // Exit
5261 
5262  return result;
5263 }
5264 
5265 bool
5267 includes_subposets(const block<pod_index_type>& xhub_ids, bool xauto_access) const
5268 {
5269  bool result = true;
5270 
5271  // Preconditions:
5272 
5273  require(state_is_auto_read_accessible(xauto_access));
5274 
5275  // Body:
5276 
5277  if(xauto_access)
5278  {
5279  get_read_access();
5280  }
5281 
5282  int i = 0;
5283  while(i < xhub_ids.ct() && result)
5284  {
5285  result = includes_subposet(xhub_ids[i], false);
5286  i++;
5287  }
5288 
5289  if(xauto_access)
5290  {
5291  release_access();
5292  }
5293 
5294  // Postconditions:
5295 
5296  ensure(unexecutable("result == for all i in xhub_ids( includes_subposet(i))"));
5297 
5298  // Exit
5299 
5300  return result;
5301 }
5302 
5303 bool
5305 includes_subposets(const block<scoped_index>& xids, bool xauto_access) const
5306 {
5307  bool result = true;
5308 
5309  // Preconditions:
5310 
5311  require(state_is_auto_read_accessible(xauto_access));
5312 
5313  // Body:
5314 
5315  if(xauto_access)
5316  {
5317  get_read_access();
5318  }
5319 
5320  int i = 0;
5321  while(i < xids.ct() && result)
5322  {
5323  result = includes_subposet(xids[i].hub_pod(), false);
5324  i++;
5325  }
5326 
5327  if(xauto_access)
5328  {
5329  release_access();
5330  }
5331 
5332  // Postconditions:
5333 
5334  ensure(unexecutable("result == for all i in xids( includes_subposet(i))"));
5335 
5336  // Exit
5337 
5338  return result;
5339 }
5340 
5343 new_subposet(bool xinitialize)
5344 {
5345  // Preconditions:
5346 
5347  require(state_is_read_write_accessible());
5348 
5349  // Body:
5350 
5351  // Get a subposet_state object from the powerset member pool.
5352 
5353  pod_index_type result = powerset().new_subposet(xinitialize);
5354 
5355  // Postconditions:
5356 
5357  ensure(invariant());
5358  ensure(includes_subposet(result, false));
5359 
5360  // Exit
5361 
5362  return result;
5363 }
5364 
5365 void
5367 new_subposet(bool xinitialize, scoped_index& result)
5368 {
5369  // Preconditions:
5370 
5371  require(state_is_read_write_accessible());
5372 
5373  // Body:
5374 
5375  // Get a subposet_state object from the powerset member pool.
5376 
5377  powerset().new_subposet(xinitialize, result);
5378 
5379  // Postconditions:
5380 
5381  ensure(invariant());
5382  ensure(includes_subposet(result, false));
5383 
5384  // Exit
5385 
5386  return;
5387 }
5388 
5392 {
5393  // Preconditions:
5394 
5395  require(state_is_read_write_accessible());
5396  require(contains_members(xmembers));
5397 
5398  // Body:
5399 
5400  // Get a subposet_state object from the powerset member pool.
5401 
5402  pod_index_type result = powerset().new_subposet(xmembers);
5403 
5404  // Postconditions:
5405 
5406  ensure(invariant());
5407  ensure(includes_subposet(result, false));
5408 
5409  // Exit
5410 
5411  return result;
5412 }
5413 
5414 void
5417 {
5418  // Preconditions:
5419 
5420  require(state_is_read_write_accessible());
5421  require(contains_members(xmembers));
5422 
5423  // Body:
5424 
5425  // Get a subposet_state object from the powerset member pool.
5426 
5427  powerset().new_subposet(xmembers, result);
5428 
5429  // Postconditions:
5430 
5431  ensure(invariant());
5432  ensure(includes_subposet(result, false));
5433 
5434  // Exit
5435 
5436  return;
5437 }
5438 
5439 void
5442 {
5443  // Preconditions:
5444 
5445  require(state_is_read_write_accessible());
5446  require(includes_subposet(xsubposet_hub_id, false));
5447 
5448  // Body:
5449 
5450  powerset().delete_subposet(xsubposet_hub_id);
5451 
5452  // Postcondition:
5453 
5454  ensure(invariant());
5455  ensure(!includes_subposet(xsubposet_hub_id, false));
5456 
5457  // Exit:
5458 
5459  return;
5460 }
5461 
5462 void
5464 delete_subposet(const scoped_index& xsubposet_id)
5465 {
5466  // Preconditions:
5467 
5468  require(state_is_read_write_accessible());
5469  require(includes_subposet(xsubposet_id, false));
5470 
5471  // Body:
5472 
5473  delete_subposet(xsubposet_id.hub_pod());
5474 
5475  // Postcondition:
5476 
5477  ensure(invariant());
5478  ensure(!includes_subposet(xsubposet_id, false));
5479 
5480  // Exit:
5481 
5482  return;
5483 }
5484 
5485 const sheaf::subposet&
5487 whole() const
5488 {
5489  require(state_is_read_accessible());
5490 
5491  return powerset().whole();
5492 }
5493 
5494 
5498 {
5499  require(state_is_read_accessible());
5500 
5501  return powerset().jims();
5502 }
5503 
5504 const sheaf::subposet&
5506 jims() const
5507 {
5508  require(state_is_read_accessible());
5509 
5510  return powerset().jims();
5511 }
5512 
5516 {
5517  require(state_is_read_accessible());
5518 
5519  return powerset().table_dof_subposet();
5520 }
5521 
5522 const sheaf::subposet&
5525 {
5526  require(state_is_read_accessible());
5527 
5528  return powerset().table_dof_subposet();
5529 }
5530 
5534 {
5535  require(state_is_read_accessible());
5536 
5537  return powerset().row_dof_subposet();
5538 }
5539 
5540 const sheaf::subposet&
5543 {
5544  require(state_is_read_accessible());
5545 
5546  return powerset().row_dof_subposet();
5547 }
5548 
5549 const std::string&
5552 {
5553  // cout << endl << "Entering poset_state_handle::coarsest_common_refinement_name." << endl;
5554 
5555  // Preconditions:
5556 
5557 
5558  // Body:
5559 
5560  // static const string result(poset_path::reserved_prefix() + "coarsest_common_refinement");
5561  static const string result("whole");
5562 
5563  // Postconditions:
5564 
5565 
5566  // Exit:
5567 
5568  // cout << "Leaving poset_state_handle::coarsest_common_refinement_name." << endl;
5569  return result;
5570 }
5571 
5572 // PROTECTED FUNCTIONS
5573 
5577 {
5578  return _resident;
5579 }
5580 
5581 const sheaf::subposet&
5583 resident() const
5584 {
5585  return _resident;
5586 }
5587 
5590 powerset() const
5591 {
5592  return *(state_obj()->powerset());
5593 }
5594 
5595 void
5597 initialize_standard_subposets(const std::string& xname)
5598 {
5599  // Preconditions:
5600 
5601  require(state_is_read_write_accessible());
5602 
5603  // Body:
5604 
5605  // Allocate the coarsest common refinement jims subposet, becomes member 0.
5606 
5607  subposet& lccr_jims = powerset().coarsest_common_refinement_jims();
5608  lccr_jims.new_state(this, true, false);
5609  lccr_jims.put_name("jims", true, false);
5610 
5611  // Allocate the coarsest common refinement whole subposet, becomes member 1
5612 
5613  subposet& lccr = powerset().coarsest_common_refinement();
5614  lccr.new_state(this, true, false);
5615  lccr.put_name(coarsest_common_refinement_name(), true, false);
5616 
5617  // CCR and version 0 are the same thing until we move to version 1.
5618 
5619  string lccr_name(version_to_name(0));
5620  lccr.put_name(lccr_name, false, false);
5621  lccr_jims.put_name(lccr_name + "_jims", false, false);
5622 
5623  // Attach the jims subposet to the coarsest common refinement jims.
5624  // poset_state_handle::jims() is reference to state_obj()->powerset_state()->jims(),
5625  // but can't use it until the latter is attached to a state.
5626 
5627  powerset().jims().attach_to_state(&lccr_jims);
5628 
5629  // Attach the whole subposet to the coarsest common refinement.
5630  // poset_state_handle::whole() is reference to state_obj()->powerset_state()->whole(),
5631  // but can't use it until the latter is attached to a state.
5632 
5633  powerset().whole().attach_to_state(&lccr);
5634 
5635  // Allocate the resident subposet, becomes member 2
5636 
5637  resident().new_state(this, true, false);
5638  resident().put_name("resident", true, false);
5639 
5640  // All the subposets are standard.
5641 
5642  put_standard_subposet_ct(subposet_ct());
5643 
5644  // Now the powerset() invariant is satisfied
5645 
5646  powerset().enable_invariant_check();
5647 
5648  // Postconditions:
5649 
5650  ensure(powerset().invariant());
5651  ensure(jims().is_attached() && jims().index() == JIMS_INDEX);
5652  ensure(whole().is_attached() && whole().index() == WHOLE_INDEX);
5653  ensure(resident().is_attached() && resident().index() == RESIDENT_INDEX);
5654  ensure(has_standard_subposet_ct());
5655 
5656  // Exit
5657 
5658  return;
5659 }
5660 
5661 void
5664 {
5665  powerset().put_standard_subposet_ct(xct);
5666 }
5667 
5668 // PRIVATE FUNCTIONS
5669 
5670 
5671 // ===========================================================
5672 // SUBPOSET NAME FACET
5673 // ===========================================================
5674 
5675 // PUBLIC MEMBER FUNCTIONS
5676 
5677 std::string
5679 subposet_name(pod_index_type xsubposet_hub_id, bool xauto_access) const
5680 {
5681  // Preconditions:
5682 
5683  require(state_is_auto_read_accessible(xauto_access));
5684 
5685  // Body:
5686 
5687  if(xauto_access)
5688  {
5689  get_read_access();
5690  }
5691 
5692 // cout << "poset_state_handle::subposet_name: poset " << name() << endl;
5693 // cout << powerset() << endl;
5694 // cout << " subposet namemap:" << endl;
5695 // cout << powerset().subposet_name_map() << endl;
5696 
5697  string result(powerset().subposet_name_map().name(xsubposet_hub_id));
5698 
5699  if(xauto_access)
5700  {
5701  release_access();
5702  }
5703 
5704  // Exit:
5705 
5706  return result;
5707 }
5708 
5709 std::string
5711 subposet_name(const scoped_index& xsubposet_id, bool xauto_access) const
5712 {
5713  // Preconditions:
5714 
5715  require(xauto_access || state_is_read_accessible());
5716 
5717  // Body:
5718 
5719  return subposet_name(xsubposet_id.hub_pod(), xauto_access);
5720 }
5721 
5722 void
5725  block<std::string>& xresult,
5726  bool xauto_access) const
5727 {
5728  // Preconditions:
5729 
5730  require(state_is_auto_read_accessible(xauto_access));
5731  require(includes_subposet(xsubposet_hub_id, xauto_access));
5732 
5733  // Body:
5734 
5735  if(xauto_access)
5736  {
5737  get_read_access();
5738  }
5739 
5740  powerset().subposet_name_map().all_names(xsubposet_hub_id, xresult);
5741 
5742  if(xauto_access)
5743  {
5744  release_access();
5745  }
5746 
5747  // Postconditions:
5748 
5749  ensure(xresult.ct() == subposet_name_ct(xsubposet_hub_id, xauto_access));
5750  ensure_for_all(i, 0, xresult.ct(), subposet_has_name(xsubposet_hub_id, xresult[i], xauto_access));
5751 
5752  // Exit:
5753 
5754  return;
5755 }
5756 
5757 void
5759 all_subposet_names(const scoped_index& xsubposet_id,
5760  block<std::string>& xresult,
5761  bool xauto_access) const
5762 {
5763  // Preconditions:
5764 
5765  require(xauto_access || state_is_read_accessible());
5766  require(includes_subposet(xsubposet_id, xauto_access));
5767 
5768  // Body:
5769 
5770  all_subposet_names(xsubposet_id.hub_pod(), xresult, xauto_access);
5771 
5772  // Postconditions:
5773 
5774  ensure(xresult.ct() == subposet_name_ct(xsubposet_id, xauto_access));
5775  ensure_for_all(i, 0, xresult.ct(), subposet_has_name(xsubposet_id, xresult[i], xauto_access));
5776 
5777  // Exit:
5778 
5779  return;
5780 }
5781 
5784 subposet_name_ct(pod_index_type xsubposet_hub_id, bool xauto_access) const
5785 {
5786  size_type result;
5787 
5788  // Preconditions:
5789 
5790  require(state_is_auto_read_accessible(xauto_access));
5791  require(includes_subposet(xsubposet_hub_id, xauto_access));
5792 
5793  // Body:
5794 
5795  if(xauto_access)
5796  {
5797  get_read_access();
5798  }
5799 
5800  result = powerset().subposet_name_map().name_ct(xsubposet_hub_id);
5801 
5802  if(xauto_access)
5803  {
5804  release_access();
5805  }
5806 
5807  // Postconditions:
5808 
5809  // Exit:
5810 
5811  return result;
5812 }
5813 
5816 subposet_name_ct(const scoped_index& xsubposet_id, bool xauto_access) const
5817 {
5818  size_type result;
5819 
5820  // Preconditions:
5821 
5822  require(xauto_access || state_is_read_accessible());
5823  require(includes_subposet(xsubposet_id, xauto_access));
5824 
5825  // Body:
5826 
5827  return subposet_name_ct(xsubposet_id.hub_pod(), xauto_access);
5828 }
5829 
5830 bool
5833  const std::string& xname,
5834  bool xauto_access) const
5835 {
5836  // Preconditions:
5837 
5838  require(state_is_auto_read_accessible(xauto_access));
5839  require(!xname.empty());
5840  require(includes_subposet(xsubposet_hub_id, xauto_access));
5841 
5842  // Body:
5843 
5844  if(xauto_access)
5845  {
5846  get_read_access();
5847  }
5848 
5849  bool result =
5850  powerset().subposet_name_map().contains_entry(xsubposet_hub_id, xname);
5851 
5852  if(xauto_access)
5853  {
5854  release_access();
5855  }
5856 
5857  // Postconditions:
5858 
5859  // Exit:
5860 
5861  return result;
5862 }
5863 
5864 bool
5866 subposet_has_name(const scoped_index& xsubposet_id,
5867  const std::string& xname,
5868  bool xauto_access) const
5869 {
5870  // Preconditions:
5871 
5872  require(xauto_access || state_is_read_accessible());
5873  require(!xname.empty());
5874  require(includes_subposet(xsubposet_id, xauto_access));
5875 
5876  // Body:
5877 
5878  return subposet_has_name(xsubposet_id.hub_pod(), xname, xauto_access);
5879 }
5880 
5881 void
5884  const std::string& xname,
5885  bool xunique,
5886  bool xauto_access)
5887 {
5888  // Preconditions:
5889 
5890  require(state_is_auto_read_write_accessible(xauto_access));
5891  require(includes_subposet(xsubposet_hub_id, xauto_access));
5892  require(poset_path::is_valid_name(xname));
5893 
5894  // Body:
5895 
5896  if(xauto_access)
5897  {
5898  get_read_write_access(true);
5899  }
5900 
5901  powerset().subposet_name_map().put_entry(xsubposet_hub_id, xname, xunique);
5902 
5903  if(xauto_access)
5904  {
5905  release_access();
5906  }
5907 
5908  // Postcondition:
5909 
5910  ensure(xunique ?
5911  (subposet_name(xsubposet_hub_id, xauto_access) == xname) :
5912  subposet_has_name(xsubposet_hub_id, xname, xauto_access));
5913 
5914  // Exit
5915 
5916  return;
5917 }
5918 
5919 void
5921 put_subposet_name(const scoped_index& xsubposet_id,
5922  const std::string& xname,
5923  bool xunique,
5924  bool xauto_access)
5925 {
5926  // Preconditions:
5927 
5928  require(xauto_access || state_is_read_write_accessible());
5929  require(includes_subposet(xsubposet_id, xauto_access));
5930  require(poset_path::is_valid_name(xname));
5931 
5932  // Body:
5933 
5934  put_subposet_name(xsubposet_id.hub_pod(), xname, xunique, xauto_access);
5935 
5936  // Postcondition:
5937 
5938  ensure(xunique ?
5939  (subposet_name(xsubposet_id, xauto_access) == xname) :
5940  subposet_has_name(xsubposet_id, xname, xauto_access));
5941 
5942  // Exit
5943 
5944  return;
5945 }
5946 
5947 void
5949 delete_subposet_name(const std::string& xname, bool xauto_access)
5950 {
5951  // Preconditions:
5952 
5953  require(!xname.empty());
5954  require(state_is_auto_read_write_accessible(xauto_access));
5955 
5956  // Body:
5957 
5958  if(xauto_access)
5959  {
5960  get_read_write_access(true);
5961  }
5962 
5963  powerset().subposet_name_map().delete_name(xname);
5964 
5965  if(xauto_access)
5966  {
5967  release_access();
5968  }
5969 
5970  // Postcondition
5971 
5972  ensure(!includes_subposet(xname, xauto_access));
5973 
5974  // Exit:
5975 
5976  return;
5977 }
5978 
5979 void
5981 delete_all_subposet_names(pod_index_type xsubposet_hub_id, bool xauto_access)
5982 {
5983  // Preconditions:
5984 
5985  require(state_is_auto_read_write_accessible(xauto_access));
5986 
5987  // Body:
5988 
5989  if(xauto_access)
5990  {
5991  get_read_write_access(true);
5992  }
5993 
5994  powerset().subposet_name_map().delete_index(xsubposet_hub_id);
5995 
5996  if(xauto_access)
5997  {
5998  release_access();
5999  }
6000 
6001  // Postcondition
6002 
6003  ensure(subposet_name_ct(xsubposet_hub_id, xauto_access) == 0);
6004 
6005  // Exit:
6006 
6007  return;
6008 }
6009 
6010 void
6012 delete_all_subposet_names(const scoped_index& xsubposet_id, bool xauto_access)
6013 {
6014  // Preconditions:
6015 
6016  require(xauto_access || state_is_read_write_accessible());
6017 
6018  // Body:
6019 
6020  delete_all_subposet_names(xsubposet_id.hub_pod(), xauto_access);
6021 
6022  // Postcondition
6023 
6024  ensure(subposet_name_ct(xsubposet_id, xauto_access) == 0);
6025 
6026  // Exit:
6027 
6028  return;
6029 }
6030 
6031 // PROTECTED MEMBER FUNCTIONS
6032 
6033 // PRIVATE MEMBER FUNCTIONS
6034 
6035 
6036 // ===========================================================
6037 // SUBPOSET ID SPACE FAMILY FACET
6038 // ===========================================================
6039 
6040 // PUBLIC FUNCTIONS
6041 
6044 subposet_id_spaces(bool xauto_access) const
6045 {
6046  // Preconditions:
6047 
6048  require(state_is_auto_read_accessible(xauto_access));
6049 
6050  // Body:
6051 
6052  if(xauto_access)
6053  {
6054  get_read_access();
6055  }
6056 
6057  const index_space_family& result = powerset()._id_spaces;
6058 
6059  if(xauto_access)
6060  {
6061  release_access();
6062  }
6063 
6064  // Postconditions:
6065 
6066  ensure(is_basic_query);
6067 
6068  // Exit:
6069 
6070  return result;
6071 }
6072 
6075 subposet_id_spaces(bool xauto_access)
6076 {
6077  // Preconditions:
6078 
6079  require(state_is_auto_read_accessible(xauto_access));
6080 
6081  // Body:
6082 
6083  if(xauto_access)
6084  {
6085  get_read_access();
6086  }
6087 
6088  index_space_family& result = powerset()._id_spaces;
6089 
6090  if(xauto_access)
6091  {
6092  release_access();
6093  }
6094 
6095  // Postconditions:
6096 
6097  ensure(is_basic_query);
6098 
6099  // Exit:
6100 
6101  return result;
6102 }
6103 
6106 subposet_hub_id_space(bool xauto_access) const
6107 {
6108  // Preconditions:
6109 
6110  require(state_is_auto_read_accessible(xauto_access));
6111 
6112  // Body:
6113 
6114  if(xauto_access)
6115  {
6116  get_read_access();
6117  }
6118 
6119  const hub_index_space_handle& result = powerset().id_spaces().hub_id_space();
6120 
6121  if(xauto_access)
6122  {
6123  release_access();
6124  }
6125 
6126  // Postconditions:
6127 
6128  ensure(result.is_attached());
6129 
6130  // Exit:
6131 
6132  return result;
6133 }
6134 
6135 const sheaf::scoped_index&
6137 subposet_id(bool xauto_access) const
6138 {
6139  // Preconditions:
6140 
6141  require(state_is_auto_read_accessible(xauto_access));
6142 
6143  // Body:
6144 
6145  if(xauto_access)
6146  {
6147  get_read_access();
6148  }
6149 
6150  const scoped_index& result = powerset().hub_id();
6151 
6152  if(xauto_access)
6153  {
6154  release_access();
6155  }
6156 
6157  // Postconditions:
6158 
6159  ensure(result.same_scope(subposet_hub_id_space(xauto_access)));
6160 
6161  // Exit:
6162 
6163  return result;
6164 }
6165 
6168 subposet_id(pod_index_type xid, bool xauto_access) const
6169 {
6170  // Preconditions:
6171 
6172  require(state_is_auto_read_accessible(xauto_access));
6173 
6174  // Body:
6175 
6176  if(xauto_access)
6177  {
6178  get_read_access();
6179  }
6180 
6181  scoped_index result(subposet_id(false));
6182  result = xid;
6183 
6184  if(xauto_access)
6185  {
6186  release_access();
6187  }
6188 
6189  // Postconditions:
6190 
6191  ensure(result.same_scope(subposet_hub_id_space(xauto_access)));
6192  ensure(result.pod() == xid);
6193 
6194  // Exit:
6195 
6196  return result;
6197 }
6198 
6199 // PROTECTED FUNCTIONS
6200 
6201 // PRIVATE FUNCTIONS
6202 
6203 
6204 // ===========================================================
6205 // SCHEMA FACET
6206 // ===========================================================
6207 
6208 // PUBLIC FUNCTIONS
6209 
6213 {
6214  // Preconditions:
6215 
6216  require(state_is_read_accessible());
6217 
6218  // Body:
6219 
6220  schema_poset_member& result = table().schema();
6221 
6222  // Postconditions:
6223 
6224  // Exit
6225 
6226  return result;
6227 }
6228 
6231 schema() const
6232 {
6233 
6234  // Preconditions:
6235 
6236  require(state_is_read_accessible());
6237 
6238  // Body:
6239 
6240  const schema_poset_member& result = table().schema();
6241 
6242  // Postconditions:
6243 
6244  // Exit
6245 
6246  return result;
6247 }
6248 
6251 schema(bool xauto_access)
6252 {
6253 
6254  // Preconditions:
6255 
6256  require(xauto_access || state_is_read_accessible());
6257 
6258  // Body:
6259 
6260  if(xauto_access)
6261  {
6262  get_read_access();
6263  }
6264 
6265  schema_poset_member& result = schema();
6266 
6267  if(xauto_access)
6268  {
6269  release_access();
6270  }
6271 
6272  // Postconditions:
6273 
6274  // Exit
6275 
6276  return result;
6277 }
6278 
6281 schema(bool xauto_access) const
6282 {
6283 
6284  // Preconditions:
6285 
6286  require(xauto_access || state_is_read_accessible());
6287 
6288  // Body:
6289 
6290  if(xauto_access)
6291  {
6292  get_read_access();
6293  }
6294 
6295  const schema_poset_member& result = schema();
6296 
6297  if(xauto_access)
6298  {
6299  release_access();
6300  }
6301 
6302  // Postconditions:
6303 
6304  // Exit
6305 
6306  return result;
6307 }
6308 
6309 bool
6311 schema_is_ancestor_of(const schema_poset_member* xother_schema) const
6312 {
6313  bool result;
6314 
6315  // Preconditions:
6316 
6317  // Body:
6318 
6319  // Always true in this class;
6320  // intended for redefinition in descendants.
6321 
6322  result = true;
6323 
6324  // Postconditions:
6325 
6326  // Exit
6327 
6328  return result;
6329 }
6330 
6331 bool
6333 schema_is(const std::string& xschema_name) const
6334 {
6335  bool result;
6336 
6337  // Preconditions:
6338 
6339  require(state_is_read_accessible());
6340 
6341  // Body:
6342 
6343  result = schema().name() == xschema_name;
6344 
6345  // Postconditions:
6346 
6347  // Exit
6348 
6349  return result;
6350 }
6351 
6352 bool
6354 same_schema(const poset_state_handle* xother) const
6355 {
6356  bool result;
6357 
6358  // Preconditions:
6359 
6360  require(state_is_read_accessible());
6361  require(xother != 0);
6362  require(xother->state_is_read_accessible());
6363 
6364  // Body:
6365 
6366  result = schema().is_same_state(&(xother->schema()));
6367 
6368  // Postconditions:
6369 
6370  // Exit
6371 
6372  return result;
6373 }
6374 
6375 bool
6378 {
6379  bool result;
6380 
6381  // Preconditions:
6382 
6383  require(state_is_read_accessible());
6384  require(xother != 0);
6385  require(xother->state_is_read_accessible());
6386 
6387 
6388  // Body:
6389 
6390  result = same_schema(xother->host());
6391 
6392  // Postconditions:
6393 
6394  // Exit
6395 
6396  return result;
6397 }
6398 
6399 
6400 // ===========================================================
6401 // TABLE DOF FACET
6402 // ===========================================================
6403 
6404 // PUBLIC MEMBER FUNCTIONS
6405 
6406 
6407 bool
6410 {
6411  bool result;
6412 
6413  // Preconditions:
6414 
6415  require(xdof_map != 0);
6416 
6417  // Body:
6418 
6419  // Table dofs must be an array_poset_dof_map.
6420 
6421  result = (dynamic_cast<const array_poset_dof_map*>(xdof_map) != 0);
6422 
6423  // Postconditions:
6424 
6425  ensure(result == (dynamic_cast<const array_poset_dof_map*>(xdof_map) != 0));
6426 
6427  // Exit
6428 
6429  return result;
6430 }
6431 
6432 bool
6434 row_dof_map_conforms(const poset_dof_map* xdof_map) const
6435 {
6436  bool result;
6437 
6438  // Preconditions:
6439 
6440  require(xdof_map != 0);
6441 
6442  // Body:
6443 
6450 
6453 
6454  // In principle any dof map will do.
6455 
6456  result = true;
6457 
6458  // Postconditions:
6459 
6460  ensure(result ? (dynamic_cast<const poset_dof_map*>(xdof_map) != 0) : true);
6461 
6462  // Exit
6463 
6464  return result;
6465 }
6466 
6469 table_dof_map(bool xrequire_write_access)
6470 {
6471  // Preconditions:
6472 
6473  require(xrequire_write_access ? state_is_read_write_accessible() : state_is_read_accessible());
6474 
6475  // Body:
6476 
6477  // Postconditions:
6478 
6479  // Exit
6480 
6481  return *(table().table_dofs());
6482 }
6483 
6486 table_dof_map(bool xrequire_write_access) const
6487 {
6488  // Preconditions:
6489 
6490  require(xrequire_write_access ? state_is_read_write_accessible() : state_is_read_accessible());
6491 
6492  // Body:
6493 
6494  // Postconditions:
6495 
6496  // Exit
6497 
6498  return *(table().table_dofs());
6499 }
6500 
6501 void
6503 table_dof_tuple(void* xbuf, size_t xbuflen) const
6504 {
6505  // Preconditions:
6506 
6507  require(state_is_read_accessible());
6508  require(schema().table_dof_tuple_ub() > 0);
6509  require(xbuflen >= schema().table_dof_tuple_ub());
6510 
6511  // Body:
6512 
6513  table_dof_map().get_dof_tuple(xbuf, xbuflen);
6514 
6515  // Postconditions:
6516 
6517  // Exit
6518 
6519  return;
6520 }
6521 
6522 void*
6525 {
6526  // Preconditions:
6527 
6528  require(state_is_read_write_accessible());
6529 
6530  // Body:
6531 
6532  void* result = table_dof_map(true).dof_tuple();
6533 
6534  // Postconditions:
6535 
6536  // Exit:
6537 
6538  return result;
6539 }
6540 
6541 const void*
6543 table_dofs() const
6544 {
6545  // Preconditions:
6546 
6547  require(state_is_read_accessible());
6548 
6549  // Body:
6550 
6551  const void* result = table_dof_map(false).dof_tuple();
6552 
6553  // Postconditions:
6554 
6555  // Exit:
6556 
6557  return result;
6558 }
6559 
6560 void*
6562 table_dofs(bool xauto_access)
6563 {
6564  // Preconditions:
6565 
6566  require(state_is_auto_read_write_accessible(xauto_access));
6567 
6568  // Body:
6569 
6570  if(xauto_access)
6571  {
6572  get_read_write_access(true);
6573  }
6574 
6575  void* result = table_dofs();
6576 
6577  if(xauto_access)
6578  {
6579  release_access();
6580  }
6581 
6582  // Postconditions:
6583 
6584 
6585  // Exit:
6586 
6587  return result;
6588 }
6589 
6590 const void*
6592 table_dofs(bool xauto_access) const
6593 {
6594  // Preconditions:
6595 
6596  require(state_is_auto_read_accessible(xauto_access));
6597 
6598  // Body:
6599 
6600  if(xauto_access)
6601  {
6602  get_read_access();
6603  }
6604 
6605  const void* result = table_dofs();
6606 
6607  if(xauto_access)
6608  {
6609  release_access();
6610  }
6611 
6612  // Postconditions:
6613 
6614  // Exit:
6615 
6616  return result;
6617 }
6618 
6621 row_dof_map(pod_index_type xtuple_hub_id, bool xrequire_write_access) const
6622 {
6623  poset_dof_map* result_ptr;
6624 
6625  // Preconditions:
6626 
6627  require(xrequire_write_access ? state_is_read_write_accessible() : state_is_read_accessible());
6628  require(contains_row_dof_tuple(xtuple_hub_id));
6629 
6630  // Body:
6631 
6632  result_ptr = table().row_dof_tuple(xtuple_hub_id);
6633 
6634  // Postconditions:
6635 
6636  // Exit
6637 
6638  return *result_ptr;
6639 }
6640 
6641 // PROTECTED MEMBER FUNCTIONS
6642 
6645 table() const
6646 {
6647  return *(state_obj()->table());
6648 }
6649 
6650 void
6652 initialize_table_dofs(void* xtable_dofs, size_t xtable_dof_ub)
6653 {
6654 
6655  // Preconditions:
6656 
6657  require(state_is_read_write_accessible());
6658  require(xtable_dofs != 0 ? xtable_dof_ub >= schema().table_dof_tuple_ub() : true);
6659 
6660 
6661  // Body:
6662 
6663  array_poset_dof_map* lmap = new array_poset_dof_map(this, true);
6664  lmap->inc_ref_ct();
6665 
6666  if((xtable_dofs != 0) && (lmap->dof_ct() > 0))
6667  {
6668  lmap->put_dof_tuple(xtable_dofs, schema().table_dof_tuple_ub());
6669  }
6670  table().put_table_dofs(lmap);
6671 
6672  // Postconditions:
6673 
6674  ensure(table().table_dofs() != 0);
6675 
6676  // Exit
6677 
6678  return;
6679 }
6680 
6681 void
6684 {
6685 
6686  // Preconditions:
6687 
6688  require(xdof_tuple != 0);
6689  require(state_is_read_write_accessible());
6690 
6691  // Body:
6692 
6693  xdof_tuple->put_host(this);
6694  xdof_tuple->inc_ref_ct();
6695  table().put_table_dofs(xdof_tuple);
6696 
6697  // Postconditions:
6698 
6699  ensure(&(table_dof_map()) == xdof_tuple);
6700 
6701  // Exit
6702 
6703  return;
6704 }
6705 
6706 // PRIVATE MEMBER FUNCTIONS
6707 
6708 // ===========================================================
6709 // ROW DOF FACET
6710 // ===========================================================
6711 
6712 // PUBLIC MEMBER FUNCTIONS
6713 
6716 row_dof_map(const scoped_index& xtuple_id, bool xrequire_write_access) const
6717 {
6718  poset_dof_map* result_ptr;
6719 
6720  // Preconditions:
6721 
6722  require(xrequire_write_access ? state_is_read_write_accessible() : state_is_read_accessible());
6723  require(contains_row_dof_tuple(xtuple_id));
6724 
6725  // Body:
6726 
6727  return row_dof_map(xtuple_id.hub_pod(), xrequire_write_access);
6728 }
6729 
6730 const sheaf::scoped_index&
6733 {
6734  // Preconditions:
6735 
6736  require(state_is_read_write_accessible());
6737 
6738  // Body:
6739 
6740  define_old_variable(int old_row_dof_tuple_ct = row_dof_tuple_ct());
6741 
6742  // Create a new dof map using contiguous array rep
6743 
6744  poset_dof_map* lmap = new array_poset_dof_map(this, false);
6745  lmap->put_defaults();
6746  table().put_row_dof_tuple(lmap);
6747  const scoped_index& result = lmap->index();
6748 
6749  // Postconditions:
6750 
6751  ensure(row_dof_tuple_ct() == old_row_dof_tuple_ct+1);
6752  ensure(contains_row_dof_tuple(result));
6753 
6754  // Exit
6755 
6756  return result;
6757 }
6758 
6759 const sheaf::scoped_index&
6762 {
6763  // Preconditions:
6764 
6765  require(state_is_read_write_accessible());
6766  require(row_dof_map_conforms(&xprototype));
6767  require(xprototype.schema().row_conforms_to(schema()));
6768 
6769  // Body:
6770 
6771  define_old_variable(int old_row_dof_tuple_ct = row_dof_tuple_ct());
6772 
6773  // Create a new dof map by copying the given prototype.
6774 
6775  poset_dof_map* lmap = xprototype.copy();
6776  lmap->put_host(this);
6777  table().put_row_dof_tuple(lmap);
6778  const scoped_index& result = lmap->index(); // Set by put_row_dof_tuple.
6779 
6780  // Postconditions:
6781 
6782  ensure(row_dof_tuple_ct() == old_row_dof_tuple_ct+1);
6783  ensure(contains_row_dof_tuple(result));
6784 
6785  // Exit
6786 
6787  return result;
6788 }
6789 
6792 member_dof_map(pod_index_type xmbr_hub_id, bool xrequire_write_access)
6793 {
6794  // Preconditions:
6795 
6796  require(xrequire_write_access ? state_is_read_write_accessible() : state_is_read_accessible());
6797  require(contains_member(xmbr_hub_id, false));
6798  require(is_jim(xmbr_hub_id, false));
6799 
6800  // Body:
6801 
6802  poset_dof_map& result =
6803  row_dof_map(member_dof_tuple_id(xmbr_hub_id, false), xrequire_write_access);
6804 
6805  // Postconditions:
6806 
6807  // Exit:
6808 
6809  return result;
6810 }
6811 
6814 member_dof_map(const scoped_index& xmbr_id, bool xrequire_write_access)
6815 {
6816  // Preconditions:
6817 
6818  require(xrequire_write_access ? state_is_read_write_accessible() : state_is_read_accessible());
6819  require(contains_member(xmbr_id, false));
6820  require(is_jim(xmbr_id, false));
6821 
6822  // Body:
6823 
6824  return member_dof_map(xmbr_id.hub_pod(), xrequire_write_access);
6825 }
6826 
6827 const sheaf::poset_dof_map&
6829 member_dof_map(pod_index_type xmbr_hub_id, bool xrequire_write_access) const
6830 {
6831  // Preconditions:
6832 
6833  require(xrequire_write_access ? state_is_read_write_accessible() : state_is_read_accessible());
6834  require(contains_member(xmbr_hub_id, false));
6835  require(is_jim(xmbr_hub_id, false));
6836 
6837  // Body:
6838 
6839  poset_dof_map& result =
6840  row_dof_map(member_dof_tuple_id(xmbr_hub_id, false), xrequire_write_access);
6841 
6842  // Postconditions:
6843 
6844  // Exit:
6845 
6846  return result;
6847 }
6848 
6849 const sheaf::poset_dof_map&
6851 member_dof_map(const scoped_index& xmbr_id, bool xrequire_write_access) const
6852 {
6853  // Preconditions:
6854 
6855  require(xrequire_write_access ? state_is_read_write_accessible() : state_is_read_accessible());
6856  require(contains_member(xmbr_id, false));
6857  require(is_jim(xmbr_id, false));
6858 
6859  // Body:
6860 
6861  return member_dof_map(xmbr_id.hub_pod(), xrequire_write_access);
6862 }
6863 
6864 void
6866 member_dof_tuple(pod_index_type xmbr_hub_id, void* xbuf, size_t xbuflen, bool xauto_access) const
6867 {
6868  // Preconditions:
6869 
6870  require(state_is_auto_read_accessible(xauto_access));
6871  require(contains_member(xmbr_hub_id, xauto_access));
6872  require(unexecutable("xbuf points to a buffer of length xbuflen"));
6873  require(xbuflen >= member_dof_map(xmbr_hub_id, false).dof_tuple_ub());
6874 
6875  // Body:
6876 
6877  if(xauto_access)
6878  {
6879  get_read_access();
6880  }
6881 
6882  member_dof_map(xmbr_hub_id, false).get_dof_tuple(xbuf, xbuflen);
6883 
6884  if(xauto_access)
6885  {
6886  release_access();
6887  }
6888 
6889  // Postconditions:
6890 
6891  // Exit
6892 
6893  return;
6894 }
6895 
6896 void
6898 put_member_dof_tuple(pod_index_type xmbr_hub_id, void* xbuf, size_t xbuflen, bool xauto_access)
6899 {
6900  // Preconditions:
6901 
6902  require(state_is_auto_read_write_accessible(xauto_access));
6903  require(contains_member(xmbr_hub_id, xauto_access));
6904  require(unexecutable("xbuf points to a buffer of length xbuflen"));
6905  require(xbuflen >= member_dof_map(xmbr_hub_id, true).dof_tuple_ub());
6906 
6907  // Body:
6908 
6909  if(xauto_access)
6910  {
6911  get_read_write_access();
6912  }
6913 
6914  member_dof_map(xmbr_hub_id, true).put_dof_tuple(xbuf, xbuflen);
6915 
6916  if(xauto_access)
6917  {
6918  release_access();
6919  }
6920 
6921  // Postconditions:
6922 
6923  // Exit
6924 
6925  return;
6926 }
6927 
6930 member_dof_tuple_id(pod_index_type xmbr_hub_id, bool xauto_access) const
6931 {
6932  // Preconditions:
6933 
6934  require(state_is_auto_read_accessible(xauto_access));
6935  require(contains_member(xmbr_hub_id, false));
6936 
6937  // Body:
6938 
6939  if(xauto_access)
6940  {
6941  get_read_access();
6942  }
6943 
6944  pod_index_type result = crg().member_dof_tuple_id(xmbr_hub_id);
6945 
6946  if(xauto_access)
6947  {
6948  release_access();
6949  }
6950 
6951  // Postconditions:
6952 
6953  ensure(!is_valid(result) || contains_row_dof_tuple(result));
6954 
6955  // Exit
6956 
6957  return result;
6958 }
6959 
6960 void
6963  scoped_index& result,
6964  bool xauto_access) const
6965 {
6966  // Preconditions:
6967 
6968  require(state_is_auto_read_accessible(xauto_access));
6969  require(contains_member(xmbr_id, false));
6970 
6971  // Body:
6972 
6973  if(xauto_access)
6974  {
6975  get_read_access();
6976  }
6977 
6978  result.put(dof_tuple_hub_id_space(false),
6979  member_dof_tuple_id(xmbr_id.hub_pod(), false));
6980 
6981  if(xauto_access)
6982  {
6983  release_access();
6984  }
6985 
6986  // Postconditions:
6987 
6988  ensure(!result.is_valid() || contains_row_dof_tuple(result));
6989 
6990  // Exit
6991 
6992  return;
6993 }
6994 
6995 void
6998  pod_index_type xtuple_hub_id,
6999  bool xauto_access)
7000 {
7001  // Preconditions:
7002 
7003  require(state_is_auto_read_write_accessible(xauto_access));
7004  require(contains_member(xmbr_hub_id, false));
7005  require(contains_row_dof_tuple(xtuple_hub_id) || !is_valid(xtuple_hub_id));
7006 
7007  // Body:
7008 
7009  if(xauto_access)
7010  {
7011  get_read_write_access(true);
7012  }
7013 
7014  crg().put_member_dof_tuple_id(xmbr_hub_id, xtuple_hub_id);
7015 
7016  if(xauto_access)
7017  {
7018  release_access();
7019  }
7020 
7021  // Postconditions:
7022 
7023  ensure(member_dof_tuple_id(xmbr_hub_id, xauto_access) == xtuple_hub_id);
7024 
7025  // Exit
7026 
7027  return;
7028 }
7029 
7030 void
7033  const scoped_index& xtuple_id,
7034  bool xauto_access)
7035 {
7036  // Preconditions:
7037 
7038  require(state_is_auto_read_write_accessible(xauto_access));
7039  require(contains_member(xmbr_id, false));
7040  require(contains_row_dof_tuple(xtuple_id) || !xtuple_id.is_valid());
7041 
7042  // Body:
7043 
7044  put_member_dof_tuple_id(xmbr_id.hub_pod(),
7045  xtuple_id.hub_pod(),
7046  xauto_access);
7047 
7048  // Postconditions:
7049 
7050  ensure(member_dof_tuple_id(xmbr_id.hub_pod(), xauto_access) == xtuple_id.hub_pod());
7051 
7052  // Exit
7053 
7054  return;
7055 }
7056 
7057 bool
7060 {
7061  bool result;
7062 
7063  // Preconditions:
7064 
7065  require(state_is_read_accessible());
7066 
7067  // Body:
7068 
7069  result = table().contains_row_dof_tuple(xtuple_hub_id);
7070 
7071  // Postconditions:
7072 
7073  // Exit
7074 
7075  return result;
7076 }
7077 
7078 bool
7080 contains_row_dof_tuple(const scoped_index& xtuple_id) const
7081 {
7082  // Preconditions:
7083 
7084  require(state_is_read_accessible());
7085 
7086  // Body:
7087 
7088  return contains_row_dof_tuple(xtuple_id.hub_pod());
7089 }
7090 
7094 {
7095  // Preconditions:
7096 
7097  require(state_is_read_accessible());
7098 
7099  // Body:
7100 
7101  int result = table().row_dof_tuple_ct();
7102 
7103  // Postconditions:
7104 
7105  ensure(result >= 0);
7106 
7107  return result;
7108 }
7109 
7110 int
7113 {
7114  int result;
7115 
7116  // Preconditions:
7117 
7118  require(state_is_read_accessible());
7119 
7120  // Body:
7121 
7122  result = table().standard_row_dof_tuple_ct();
7123 
7124  // Postconditions:
7125 
7126  ensure(result >= 0);
7127 
7128  // Exit:
7129 
7130  return result;
7131 }
7132 
7133 bool
7136 {
7137  bool result;
7138 
7139  // Preconditions:
7140 
7141  require(state_is_read_accessible());
7142 
7143  // Body:
7144 
7145  result = (row_dof_tuple_ct() == standard_row_dof_tuple_ct());
7146 
7147  // Postconditions:
7148 
7149  ensure(result == (row_dof_tuple_ct() == standard_row_dof_tuple_ct()));
7150 
7151  return result;
7152 }
7153 
7154 // PROTECTED MEMBER FUNCTIONS
7155 
7156 // PRIVATE MEMBER FUNCTIONS
7157 
7158 
7159 // PROTECTED FUNCTIONS
7160 
7161 // PRIVATE FUNCTIONS
7162 
7163 
7164 // ===========================================================
7165 // DOF TUPLE ID SPACE FAMILY FACET
7166 // ===========================================================
7167 
7168 // PUBLIC FUNCTIONS
7169 
7172 dof_tuple_id_spaces(bool xauto_access) const
7173 {
7174  // Preconditions:
7175 
7176  require(state_is_auto_read_accessible(xauto_access));
7177 
7178  // Body:
7179 
7180  if(xauto_access)
7181  {
7182  get_read_access();
7183  }
7184 
7185  const index_space_family& result = table()._id_spaces;
7186 
7187  if(xauto_access)
7188  {
7189  release_access();
7190  }
7191 
7192  // Postconditions:
7193 
7194  ensure(is_basic_query);
7195 
7196  // Exit:
7197 
7198  return result;
7199 }
7200 
7203 dof_tuple_id_spaces(bool xauto_access)
7204 {
7205  // Preconditions:
7206 
7207  require(state_is_auto_read_accessible(xauto_access));
7208 
7209  // Body:
7210 
7211  if(xauto_access)
7212  {
7213  get_read_access();
7214  }
7215 
7216  index_space_family& result = table()._id_spaces;
7217 
7218  if(xauto_access)
7219  {
7220  release_access();
7221  }
7222 
7223  // Postconditions:
7224 
7225  ensure(is_basic_query);
7226 
7227  // Exit:
7228 
7229  return result;
7230 }
7231 
7234 dof_tuple_hub_id_space(bool xauto_access) const
7235 {
7236  // Preconditions:
7237 
7238  require(state_is_auto_read_accessible(xauto_access));
7239 
7240  // Body:
7241 
7242  if(xauto_access)
7243  {
7244  get_read_access();
7245  }
7246 
7247  const hub_index_space_handle& result = table().id_spaces().hub_id_space();
7248 
7249  if(xauto_access)
7250  {
7251  release_access();
7252  }
7253 
7254  // Postconditions:
7255 
7256  ensure(result.is_attached());
7257 
7258  // Exit:
7259 
7260  return result;
7261 }
7262 
7263 const sheaf::scoped_index&
7265 dof_tuple_id(bool xauto_access) const
7266 {
7267  // Preconditions:
7268 
7269  require(state_is_auto_read_accessible(xauto_access));
7270 
7271  // Body:
7272 
7273  if(xauto_access)
7274  {
7275  get_read_access();
7276  }
7277 
7278  const scoped_index& result = table().hub_id();
7279 
7280  if(xauto_access)
7281  {
7282  release_access();
7283  }
7284 
7285  // Postconditions:
7286 
7287  ensure(result.same_scope(dof_tuple_hub_id_space(xauto_access)));
7288 
7289  // Exit:
7290 
7291  return result;
7292 }
7293 
7296 dof_tuple_id(pod_index_type xid, bool xauto_access) const
7297 {
7298  // Preconditions:
7299 
7300  require(state_is_auto_read_accessible(xauto_access));
7301 
7302  // Body:
7303 
7304  if(xauto_access)
7305  {
7306  get_read_access();
7307  }
7308 
7309  scoped_index result(dof_tuple_id(false));
7310  result = xid;
7311 
7312  if(xauto_access)
7313  {
7314  release_access();
7315  }
7316 
7317  // Postconditions:
7318 
7319  ensure(result.same_scope(dof_tuple_hub_id_space(xauto_access)));
7320  ensure(result.pod() == xid);
7321 
7322  // Exit:
7323 
7324  return result;
7325 }
7326 
7327 // PROTECTED FUNCTIONS
7328 
7329 // PRIVATE FUNCTIONS
7330 
7331 
7332 // ===========================================================
7333 // SCHEMATIZATION FACET
7334 // ===========================================================
7335 
7336 // PUBLIC FUNCTIONS
7337 
7338 bool
7340 is_schematized(bool xauto_access) const
7341 {
7342  bool result;
7343 
7344  // Preconditions:
7345 
7346  require(state_is_auto_read_accessible(xauto_access));
7347 
7348  // Body:
7349 
7350  if(xauto_access)
7351  {
7352  get_read_access();
7353  }
7354 
7355  result = includes_subposet(schema_poset_member::table_dof_subposet_name("top")) &&
7356  includes_subposet(schema_poset_member::row_dof_subposet_name("top"));
7357 
7358  if(xauto_access)
7359  {
7360  release_access();
7361  }
7362 
7363  // Postconditions:
7364 
7366 
7367  ensure(unexecutable(result == top member has been schematized));
7368 
7369  // Exit
7370 
7371  return result;
7372 }
7373 
7374 void
7376 schematize(subposet* xtable_dof_subposet,
7377  subposet* xrow_dof_subposet,
7378  bool xall_members)
7379 {
7380  // Preconditions:
7381 
7382  require(state_is_read_write_accessible());
7383  require(xtable_dof_subposet != 0);
7384  require(includes_subposet(xtable_dof_subposet));
7385  require(xrow_dof_subposet != 0);
7386  require(includes_subposet(xrow_dof_subposet));
7387 
7388  // Body:
7389 
7390  string ltop_table_dof_sp_name(schema_poset_member::table_dof_subposet_name("top"));
7391  if(xtable_dof_subposet->name() != ltop_table_dof_sp_name)
7392  {
7393  xtable_dof_subposet->put_name(ltop_table_dof_sp_name, true, false);
7394  }
7395  table_dof_subposet().attach_to_state(xtable_dof_subposet, false);
7396 
7397  if(!table_dof_subposet().has_id_space())
7398  {
7399  initialize_dof_id_space(table_dof_subposet());
7400  }
7401 
7402  string ltop_row_dof_sp_name(schema_poset_member::row_dof_subposet_name("top"));
7403  if(xrow_dof_subposet->name() != ltop_row_dof_sp_name)
7404  {
7405  xrow_dof_subposet->put_name(ltop_row_dof_sp_name, true, false);
7406  }
7407  row_dof_subposet().attach_to_state(xrow_dof_subposet, false);
7408 
7409  if(!row_dof_subposet().has_id_space())
7410  {
7411  initialize_dof_id_space(row_dof_subposet());
7412  }
7413 
7414  // Postconditions:
7415 
7416  ensure(is_schematized(false));
7417 
7418  // Exit
7419 
7420  return;
7421 }
7422 
7423 // PROTECTED FUNCTIONS
7424 
7425 void
7428 {
7429  // Preconditions:
7430 
7431  require(state_is_read_write_accessible());
7432 
7433  // Body:
7434 
7435  xdof_subposet.put_is_persistent(true);
7436  if(member_id_spaces(false).contains(xdof_subposet.id_space_name()))
7437  {
7438  xdof_subposet.attach_id_space();
7439  }
7440  else
7441  {
7442  xdof_subposet.new_id_space("array_index_space_state");
7443 
7444  scattered_insertion_index_space_handle& ldof_id_space = xdof_subposet.id_space();
7445 
7446  index_iterator ldof_itr = xdof_subposet.indexed_member_iterator();
7447  while(!ldof_itr.is_done())
7448  {
7449  ldof_id_space.push_back(ldof_itr.index());
7450 
7451  ldof_itr.next();
7452  }
7453  }
7454 
7455  // Postconditions:
7456 
7457  ensure(xdof_subposet.has_id_space());
7458 
7459  // Exit:
7460 
7461  return;
7462 }
7463 
7464 // PRIVATE FUNCTIONS
7465 
7466 
7467 
7468 
7469 // ===========================================================
7470 // VERSION FACET
7471 // ===========================================================
7472 
7473 // PUBLIC FUNCTIONS
7474 
7475 int
7477 version_ct() const
7478 {
7479  int result = 0;
7480 
7481  // Preconditions:
7482 
7483  // Body:
7484 
7488 
7489 // subposet sp;
7490 
7491 // index_iterator itr = subposet_iterator();
7492 // while(!itr.is_done())
7493 // {
7494 // sp.attach_to_state(this, itr.index());
7495 
7496 // // Count all subposets with names beginning with "__version_".
7497 
7498 // if(is_version_name(sp.name()))
7499 // {
7500 // result++;
7501 // }
7502 
7503 // itr.next();
7504 // }
7505 // sp.detach_from_state();
7506 
7507 
7508  typedef poset_powerset_state::subposet_name_map_type name_map_type;
7509  typedef name_map_type::const_iterator name_map_itr_type;
7510  typedef name_map_type::const_name_iterator name_itr_type;
7511 
7512  for(name_map_itr_type lmap_itr = powerset().subposet_name_map().begin();
7513  lmap_itr != powerset().subposet_name_map().end();
7514  ++lmap_itr)
7515  {
7516  for(name_itr_type lname_itr = lmap_itr->second.begin();
7517  lname_itr != lmap_itr->second.end();
7518  ++lname_itr)
7519  {
7520  if(is_version_name(*lname_itr))
7521  {
7522  result++;
7523  }
7524  }
7525  }
7526 
7527  // Have now double counted the levels, because each
7528  // level has a whole subposet and a jims subposet.
7529 
7530  assertion(result % 2 == 0);
7531 
7532  result = result/2;
7533 
7534  // Have also counted
7535 
7536  ensure(result >= 0);
7537 
7538  // Exit
7539 
7540  return result;
7541 }
7542 
7543 int
7545 version() const
7546 {
7547  int result;
7548 
7549  // Preconditions:
7550 
7551  require(state_is_read_accessible());
7552 
7553  // Body:
7554 
7555  result = version_from_name(whole().name());
7556 
7557  // Postconditions:
7558 
7559  // Exit
7560 
7561  return result;
7562 }
7563 
7566 version_index(int xversion) const
7567 {
7568  pod_index_type result;
7569 
7570  // Preconditions:
7571 
7572  require(state_is_read_accessible());
7573  require(has_version(xversion));
7574 
7575  // Body:
7576 
7577  if(xversion == CURRENT_HOST_VERSION)
7578  {
7579  result = WHOLE_INDEX;
7580  }
7581  else
7582  {
7583  string lvl_name = version_to_name(xversion);
7584  result = subposet_id(lvl_name);
7585  }
7586 
7587  // Postconditions:
7588 
7589  ensure(includes_subposet(result, false));
7590 
7591  // Exit
7592 
7593  return result;
7594 }
7595 
7596 void
7598 version_index(int xversion, scoped_index& result) const
7599 {
7600  // Preconditions:
7601 
7602  require(state_is_read_accessible());
7603  require(has_version(xversion));
7604 
7605  // Body:
7606 
7607  result.put(subposet_hub_id_space(false), version_index(xversion));
7608 
7609  // Postconditions:
7610 
7611  ensure(includes_subposet(result, false));
7612 
7613  // Exit
7614 
7615  return;
7616 }
7617 
7620 version_jims_index(int xversion) const
7621 {
7622  // Preconditions:
7623 
7624  require(state_is_read_accessible());
7625  require(has_version(xversion));
7626 
7627  // Body:
7628 
7629  string lvl_name = version_to_name(xversion);
7630  lvl_name += "_jims";
7631  pod_index_type result = subposet_id(lvl_name);
7632 
7633  // Postconditions:
7634 
7635  ensure(includes_subposet(result));
7636 
7637  // Exit
7638 
7639  return result;
7640 }
7641 
7642 void
7644 version_jims_index(int xversion, scoped_index& result) const
7645 {
7646  // Preconditions:
7647 
7648  require(state_is_read_accessible());
7649  require(has_version(xversion));
7650 
7651  // Body:
7652 
7653  result.put(subposet_hub_id_space(false), version_jims_index(xversion));
7654 
7655  // Postconditions:
7656 
7657  ensure(includes_subposet(result));
7658 
7659  // Exit
7660 
7661  return;
7662 }
7663 
7664 bool
7666 has_version( int xversion ) const
7667 {
7668  bool result;
7669 
7670  // Preconditions:
7671 
7672  // Body:
7673 
7674  result = ( (xversion == CURRENT_HOST_VERSION) ||
7675  ( (0 <= xversion) && (xversion < version_ct()) ) ||
7676  (xversion == COARSEST_COMMON_REFINEMENT_VERSION) );
7677 
7678  // Postconditions:
7679 
7680  // Exit
7681 
7682  return result;
7683 }
7684 
7685 bool
7687 is_version() const
7688 {
7689  bool result;
7690 
7691  // Preconditions:
7692 
7693  // Body:
7694 
7695  result = version() != COARSEST_COMMON_REFINEMENT_VERSION;
7696 
7697  // Postconditions:
7698 
7699  // Exit
7700 
7701  return result;
7702 }
7703 
7704 // PROTECTED FUNCTIONS
7705 
7706 const std::string&
7709 {
7710  static const string result("__version_");
7711  return result;
7712 }
7713 
7714 int
7717 {
7718  static const int result = VERSION_PREFIX().size();
7719  return result;
7720 }
7721 
7722 bool
7724 is_version_name(const std::string& xname) const
7725 {
7726  bool result;
7727 
7728  // Preconditions:
7729 
7730  // Body:
7731 
7732  // Coarsest_common_refinement has same name as this.
7733  // Other version names have form "__version_n";
7734  // number n begins at character position 10.
7735 
7736  result = (xname.substr(0, VERSION_PREFIX_LENGTH()) == VERSION_PREFIX());
7737 
7738  // Postconditions:
7739 
7740  // Exit
7741 
7742  return result;
7743 }
7744 
7745 std::string
7746 sheaf::