Source code

001// ***** This file is automatically generated from OneOf.java.jpp
002
003package daikon.inv.unary.sequence;
004
005import daikon.*;
006import daikon.inv.*;
007import daikon.inv.unary.OneOf;
008
009  import daikon.inv.binary.twoSequence.SubSequence;
010  import daikon.inv.unary.scalar.*;
011
012import java.io.*;
013import java.util.logging.Logger;
014import java.util.logging.Level;
015import java.util.*;
016
017import org.checkerframework.checker.initialization.qual.Initialized;
018import org.checkerframework.checker.interning.qual.Interned;
019import org.checkerframework.checker.lock.qual.GuardSatisfied;
020import org.checkerframework.checker.nullness.qual.NonNull;
021import org.checkerframework.checker.nullness.qual.Nullable;
022import org.checkerframework.dataflow.qual.Pure;
023import org.checkerframework.dataflow.qual.SideEffectFree;
024import org.checkerframework.framework.qual.Unused;
025import org.plumelib.reflection.Signatures;
026import org.plumelib.util.ArraysPlume;
027import org.plumelib.util.Intern;
028import org.plumelib.util.StringsPlume;
029import org.plumelib.util.UtilPlume;
030import typequals.prototype.qual.NonPrototype;
031import typequals.prototype.qual.Prototype;
032
033// This subsumes an "exact" invariant that says the value is always exactly
034// a specific value.  Do I want to make that a separate invariant
035// nonetheless?  Probably not, as this will simplify implication and such.
036
037  /**
038   * Represents sequences of double values where the elements of the sequence take on only a
039   * few distinct values. Prints as either {@code x[] elements == c} (when there is only one value),
040   * or as {@code x[] elements one of {c1, c2, c3}} (when there are multiple values).
041
042   */
043
044@SuppressWarnings("UnnecessaryParentheses")  // generated code, parentheses are sometimes needed
045public final class EltOneOfFloat extends SingleFloatSequence implements OneOf {
046  // We are Serializable, so we specify a version to allow changes to
047  // method signatures without breaking serialization.  If you add or
048  // remove fields, you should change this number to the current date.
049  static final long serialVersionUID = 20030822L;
050
051  /** Debugging logger. */
052  public static final Logger debug =
053    Logger.getLogger(EltOneOfFloat.class.getName());
054
055  // Variables starting with dkconfig_ should only be set via the
056  // daikon.config.Configuration interface.
057  /** Boolean. True iff OneOf invariants should be considered. */
058  public static boolean dkconfig_enabled = Invariant.invariantEnabledDefault;
059
060  /**
061   * Positive integer. Specifies the maximum set size for this type of invariant (x is one of
062   * {@code size} items).
063   */
064
065  public static int dkconfig_size = 3;
066
067  // Probably needs to keep its own list of the values, and number of each seen.
068  // (That depends on the slice; maybe not until the slice is cleared out.
069  // But so few values is cheap, so this is quite fine for now and long-term.)
070
071  @Unused(when=Prototype.class)
072  private double[] elts;
073  @Unused(when=Prototype.class)
074  private int num_elts;
075
076  @Prototype EltOneOfFloat() {
077    super();
078  }
079
080  EltOneOfFloat(PptSlice slice) {
081    super(slice);
082
083    elts = new double[dkconfig_size];
084
085    num_elts = 0;
086
087    // var() is initialized by the super constructor
088    assert var().is_array() :
089      String.format("In %s constructor, var %s (type=%s, rep_type=%s) should be an array",
090                     "EltOneOfFloat", var().name(), var().type, var().rep_type);
091
092  }
093
094  private static @Prototype EltOneOfFloat proto = new @Prototype EltOneOfFloat();
095
096  /** Returns the prototype invariant for EltOneOfFloat */
097  public static @Prototype EltOneOfFloat get_proto() {
098    return proto;
099  }
100
101  /** returns whether or not this invariant is enabled */
102  @Override
103  public boolean enabled() {
104    return dkconfig_enabled;
105  }
106
107  /** instantiate an invariant on the specified slice */
108  @Override
109  public EltOneOfFloat instantiate_dyn(@Prototype EltOneOfFloat this, PptSlice slice) {
110    return new EltOneOfFloat(slice);
111  }
112
113  @Pure
114  public boolean is_boolean(@GuardSatisfied EltOneOfFloat this) {
115    return var().file_rep_type.elementType() == ProglangType.BOOLEAN;
116  }
117  @Pure
118  public boolean is_hashcode(@GuardSatisfied EltOneOfFloat this) {
119    return var().file_rep_type.elementType() == ProglangType.HASHCODE;
120  }
121
122  @SideEffectFree
123  @Override
124  public EltOneOfFloat clone(@GuardSatisfied EltOneOfFloat this) {
125    EltOneOfFloat result = (EltOneOfFloat) super.clone();
126    result.elts = elts.clone();
127
128    result.num_elts = this.num_elts;
129    return result;
130  }
131
132  @Override
133  public int num_elts() {
134    return num_elts;
135  }
136
137  @Override
138  public Object elt() {
139    return elt(0);
140  }
141
142  public Object elt(int index) {
143    if (num_elts <= index) {
144      throw new Error("Represents " + num_elts + " elements, index " + index + " not valid");
145    }
146
147    return Intern.internedDouble(elts[index]);
148  }
149
150  private void sort_rep(@GuardSatisfied EltOneOfFloat this) {
151    Arrays.sort(elts, 0, num_elts );
152  }
153
154  public double min_elt() {
155    if (num_elts == 0) {
156      throw new Error("Represents no elements");
157    }
158    sort_rep();
159    return elts[0];
160  }
161
162  public double max_elt() {
163    if (num_elts == 0) {
164      throw new Error("Represents no elements");
165    }
166    sort_rep();
167    return elts[num_elts - 1];
168  }
169
170  // Assumes the other array is already sorted
171  public boolean compare_rep(int num_other_elts, double[] other_elts) {
172    if (num_elts != num_other_elts) {
173      return false;
174    }
175    sort_rep();
176    for (int i = 0; i < num_elts; i++) {
177      if (!(Global.fuzzy.eq(elts[i], other_elts[i]) || (Double.isNaN(elts[i]) && Double.isNaN(other_elts[i])))) { // elements are interned
178        return false;
179      }
180    }
181    return true;
182  }
183
184  private String subarray_rep(@GuardSatisfied EltOneOfFloat this) {
185    // Not so efficient an implementation, but simple;
186    // and how often will we need to print this anyway?
187    sort_rep();
188    StringBuilder sb = new StringBuilder();
189    sb.append("{ ");
190    for (int i = 0; i < num_elts; i++) {
191      if (i != 0) {
192        sb.append(", ");
193      }
194
195      if (PrintInvariants.dkconfig_static_const_infer) {
196        boolean curVarMatch = false;
197        PptTopLevel pptt = ppt.parent;
198        for (VarInfo vi : pptt.var_infos) {
199          if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
200            // If variable is a double, then use fuzzy comparison
201            if (vi.rep_type == ProglangType.DOUBLE) {
202              Double constantVal = (Double)vi.constantValue();
203              if (Global.fuzzy.eq(constantVal, elts[i]) || (Double.isNaN(constantVal) && Double.isNaN(elts[i]))) {
204                sb.append(vi.name());
205                curVarMatch = true;
206              }
207            }
208            // Otherwise just use the equals method
209            else {
210              Object constantVal = vi.constantValue();
211              if (constantVal.equals(elts[i])) {
212                sb.append(vi.name());
213                curVarMatch = true;
214              }
215            }
216          }
217        }
218
219        if (curVarMatch == false) {
220          sb.append((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
221        }
222      } else {
223        sb.append((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
224      }
225
226    }
227    sb.append(" }");
228    return sb.toString();
229  }
230
231  @Override
232  public String repr(@GuardSatisfied EltOneOfFloat this) {
233    return "EltOneOfFloat" + varNames() + ": falsified=" + falsified
234      + ", num_elts=" + num_elts
235      + ", elts=" + subarray_rep();
236  }
237
238  @SideEffectFree
239  @Override
240  public String format_using(@GuardSatisfied EltOneOfFloat this, OutputFormat format) {
241    sort_rep();
242
243    if (format.isJavaFamily()) {
244      return format_java_family(format);
245    }
246
247    if (format == OutputFormat.DAIKON) {
248      return format_daikon();
249    } else if (format == OutputFormat.SIMPLIFY) {
250      return format_simplify();
251    } else if (format == OutputFormat.ESCJAVA) {
252      String result = format_esc();
253      return result;
254    } else if (format == OutputFormat.CSHARPCONTRACT) {
255      return format_csharp_contract();
256    } else {
257      return format_unimplemented(format);
258    }
259  }
260
261  public String format_daikon(@GuardSatisfied EltOneOfFloat this) {
262    String varname = var().name() + " elements";
263    if (num_elts == 1) {
264
265        if (PrintInvariants.dkconfig_static_const_infer) {
266          PptTopLevel pptt = ppt.parent;
267          for (VarInfo vi : pptt.var_infos) {
268            if (vi.isStaticConstant() && VarComparability.comparable(vi, var())) {
269              if (vi.rep_type == ProglangType.DOUBLE) {
270                Double constantVal = (Double)vi.constantValue();
271                if (Global.fuzzy.eq(constantVal, elts[0]) || (Double.isNaN(constantVal) && Double.isNaN(elts[0]))) {
272                  return varname + " == " + vi.name();
273                }
274              } else {
275                Object constantVal = vi.constantValue();
276                if (constantVal.equals(elts[0])) {
277                  return varname + " == " + vi.name();
278                }
279              }
280            }
281          }
282        }
283        return varname + " == " + (Double.isNaN(elts[0]) ? "Double.NaN" : String.valueOf(elts[0]));
284    } else {
285      return varname + " one of " + subarray_rep();
286    }
287  }
288
289  public String format_esc(@GuardSatisfied EltOneOfFloat this) {
290    sort_rep();
291
292    String[] form = VarInfo.esc_quantify(var());
293    String varname = form[1];
294
295    String result;
296
297    {
298      result = "";
299      for (int i = 0; i < num_elts; i++) {
300        if (i != 0) { result += " || "; }
301        result += varname + " == " + (Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i]));
302      }
303    }
304
305    result = form[0] + "(" + result + ")" + form[2];
306
307    return result;
308  }
309
310public String format_csharp_contract(@GuardSatisfied EltOneOfFloat this) {
311
312    @NonNull @Initialized String result;
313
314    String equalsString = " == ";
315    String endString = "";
316
317    String[] split = var().csharp_array_split();
318    List<String> args_list = new ArrayList<>();
319    // Construct the array that unary value will be compared against.
320    for (int i = 0; i < num_elts; i++) {
321
322      args_list.add((Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i])));
323
324    }
325    String args = String.join(", ", args_list);
326
327    if (num_elts == 0) { // If there are no elements, length must be 0.
328      String varname = var().csharp_name();
329      return varname + ".Count() == 0";
330    } else if (num_elts == 1) {
331
332      {
333        result = "Contract.ForAll(" + split[0] + ", x => x" + split[1] + equalsString + args + endString + ")";
334      }
335    } else {
336      assert num_elts > 1;
337      result = "Contract.ForAll(" + split[0] + ", x => x" + split[1] + ".OneOf(" + args + "))";
338    }
339
340    return result;
341  }
342
343  public String format_java_family(@GuardSatisfied EltOneOfFloat this, OutputFormat format) {
344
345    String result;
346
347    // Setting up the name of the unary variable
348    String varname = var().name_using(format);
349
350    // Constructing the array that unary val will be compared against
351
352    String oneOfArray = "new double[] { ";
353
354    for (int i = 0 ; i < num_elts ; i++) {
355      if (i != 0) { oneOfArray += ", "; }
356      oneOfArray = oneOfArray + (Double.isNaN(elts[i]) ? "Double.NaN" : String.valueOf(elts[i]));
357    }
358    oneOfArray += " }";
359
360    // Calling quantification method
361    if (num_elts == 1) {
362
363        {
364          result = "daikon.Quant.eltsEqual(" + varname + ", "
365            + (Double.isNaN(elts[0]) ? "Double.NaN" : String.valueOf(elts[0])) + ")";
366        }
367    } else {
368      assert num_elts > 1;
369      // eltsOneOf == subsetOf
370      result = "daikon.Quant.subsetOf(" + varname + ", " + oneOfArray + ")";
371    }
372
373    return result;
374  }
375
376  public String format_simplify(@GuardSatisfied EltOneOfFloat this) {
377
378    sort_rep();
379
380    String[] form = VarInfo.simplify_quantify(var());
381    String varname = form[1];
382
383    String result;
384
385    {
386      result = "";
387      for (int i = 0; i < num_elts; i++) {
388        result += " (EQ " + varname + " " + simplify_format_double(elts[i]) + ")";
389      }
390      if (num_elts > 1) {
391        result = "(OR" + result + ")";
392      } else if (num_elts == 1) {
393        // chop leading space
394        result = result.substring(1);
395      } else {
396        // Haven't actually seen any data, so we're vacuously true
397        return format_too_few_samples(OutputFormat.SIMPLIFY, null);
398      }
399    }
400
401    result = form[0] + result + form[2];
402
403    if (result.indexOf("format_simplify") == -1) {
404      daikon.simplify.SimpUtil.assert_well_formed(result);
405    }
406    return result;
407  }
408
409  @Override
410  public InvariantStatus add_modified(double[] a, int count) {
411    return runValue(a, count, true);
412  }
413
414  @Override
415  public InvariantStatus check_modified(double[] a, int count) {
416    return runValue(a, count, false);
417  }
418
419  private InvariantStatus runValue(double[] a, int count, boolean mutate) {
420    InvariantStatus finalStatus = InvariantStatus.NO_CHANGE;
421    for (int ai = 0; ai <a.length; ai++) {
422      InvariantStatus status;
423      if (mutate) {
424        status = add_mod_elem(a[ai], count);
425      } else {
426        status = check_mod_elem(a[ai], count);
427      }
428      if (status == InvariantStatus.FALSIFIED) {
429        return InvariantStatus.FALSIFIED;
430      } else if (status == InvariantStatus.WEAKENED) {
431        finalStatus = InvariantStatus.WEAKENED;
432      }
433    }
434    return finalStatus;
435  }
436
437  /**
438   * Adds a single sample to the invariant. Returns
439   * the appropriate InvariantStatus from the result
440   * of adding the sample to this.
441   */
442  public InvariantStatus add_mod_elem(double v, int count) {
443    InvariantStatus status = check_mod_elem(v, count);
444    if (status == InvariantStatus.WEAKENED) {
445      elts[num_elts] = v;
446      num_elts++;
447    }
448    return status;
449  }
450
451  /**
452   * Checks a single sample to the invariant. Returns
453   * the appropriate InvariantStatus from the result
454   * of adding the sample to this.
455   */
456  public InvariantStatus check_mod_elem(double v, int count) {
457
458    // Look for v in our list of previously seen values.  If it's
459    // found, we're all set.
460    for (int i = 0; i < num_elts; i++) {
461      // if (logDetail())
462      //  log ("add_modified (" + v + ")");
463      if ((Global.fuzzy.eq(elts[i], v) || (Double.isNaN(elts[i]) && Double.isNaN( v)))) {
464        return InvariantStatus.NO_CHANGE;
465      }
466    }
467
468    if (num_elts == dkconfig_size) {
469      return InvariantStatus.FALSIFIED;
470    }
471
472    return InvariantStatus.WEAKENED;
473  }
474
475  // It is possible to have seen many (array) samples, but no (double)
476  // array element values.
477  @Override
478  public boolean enoughSamples(@GuardSatisfied EltOneOfFloat this) {
479    return num_elts > 0;
480  }
481
482  @Override
483  protected double computeConfidence() {
484    // This is not ideal.
485    if (num_elts == 0) {
486      return Invariant.CONFIDENCE_UNJUSTIFIED;
487    } else {
488      return Invariant.CONFIDENCE_JUSTIFIED;
489    }
490  }
491
492  @Pure
493  @Override
494  public @Nullable DiscardInfo isObviousStatically(VarInfo[] vis) {
495    // Static constants are necessarily OneOf precisely one value.
496    // This removes static constants from the output, which might not be
497    // desirable if the user doesn't know their actual value.
498    if (vis[0].isStaticConstant()) {
499      assert num_elts <= 1;
500      return new DiscardInfo(this, DiscardCode.obvious, vis[0].name() + " is a static constant.");
501    }
502    return super.isObviousStatically(vis);
503  }
504
505  @Pure
506  @Override
507  public @Nullable DiscardInfo isObviousDynamically(VarInfo[] vis) {
508    DiscardInfo super_result = super.isObviousDynamically(vis);
509    if (super_result != null) {
510      return super_result;
511    }
512
513    VarInfo v = vis[0];
514
515    // We can check if all values in the list match with the ones we know about
516    // (useful for booleans and numeric enumerations).
517    if (v.aux.hasValue(VarInfoAux.VALID_VALUES)) {
518      String[] vsValidValues         = v.aux.getList(VarInfoAux.VALID_VALUES);
519      Set<Double> setValidValues = new TreeSet<>();
520      for (String s : vsValidValues) {
521        setValidValues.add(Double.valueOf(s));
522      }
523      Set<Double> setValuesInvariant = new TreeSet<>();
524      for (double e : elts) {
525        setValuesInvariant.add(e);
526      }
527      if (setValidValues.equals(setValuesInvariant)) {
528        return new DiscardInfo(this, DiscardCode.obvious,
529          "The value list matches the allowed value list");
530      }
531    }
532
533    // Look for the same property over a supersequence of this one.
534    PptTopLevel pptt = ppt.parent;
535    for (Iterator<Invariant> inv_itor = pptt.invariants_iterator(); inv_itor.hasNext(); ) {
536      Invariant inv = inv_itor.next();
537      if (inv == this) {
538        continue;
539      }
540      if (inv instanceof EltOneOfFloat) {
541        EltOneOfFloat other = (EltOneOfFloat) inv;
542        if (isSameFormula(other)
543          && SubSequence.isObviousSubSequenceDynamically(this, v, other.var())) {
544          debug.fine("isObviousDyn: Returning true because isObviousSubSequenceDynamically");
545          return new DiscardInfo(this, DiscardCode.obvious, "The same property holds over a supersequence " + other.var().name());
546        }
547      }
548    }
549
550    return null;
551  }
552
553  /**
554   * Oneof can merge different formulas from lower points to create a single formula at an upper
555   * point.
556   */
557  @Override
558  public boolean mergeFormulasOk() {
559    return true;
560  }
561
562  @Pure
563  @Override
564  public boolean isSameFormula(Invariant o) {
565    EltOneOfFloat other = (EltOneOfFloat) o;
566    if (num_elts != other.num_elts) {
567      return false;
568    }
569    if (num_elts == 0 && other.num_elts == 0) {
570      return true;
571    }
572
573    sort_rep();
574    other.sort_rep();
575
576    for (int i = 0; i < num_elts; i++) {
577      if (!(Global.fuzzy.eq(elts[i], other.elts[i]) || (Double.isNaN(elts[i]) && Double.isNaN(other.elts[i])))) {
578        return false;
579      }
580    }
581
582    return true;
583  }
584
585  @Pure
586  @Override
587  public boolean isExclusiveFormula(Invariant o) {
588    if (o instanceof EltOneOfFloat) {
589      EltOneOfFloat other = (EltOneOfFloat) o;
590
591      if (num_elts == 0 || other.num_elts == 0) {
592        return false;
593      }
594      for (int i = 0; i < num_elts; i++) {
595        for (int j = 0; j < other.num_elts; j++) {
596          if ((Global.fuzzy.eq(elts[i], other.elts[j]) || (Double.isNaN(elts[i]) && Double.isNaN(other.elts[j])))) // elements are interned
597            return false;
598        }
599      }
600
601      return true;
602    }
603
604    // Many more checks can be added here:  against nonzero, modulus, etc.
605    if ((o instanceof EltNonZeroFloat) && (num_elts == 1) && (elts[0] == 0)) {
606      return true;
607    }
608    double elts_min = Double.MAX_VALUE;
609    double elts_max = Double.MIN_VALUE;
610    for (int i = 0; i < num_elts; i++) {
611      elts_min = Math.min(elts_min, elts[i]);
612      elts_max = Math.max(elts_max, elts[i]);
613    }
614    if ((o instanceof LowerBoundFloat) && (elts_max < ((LowerBoundFloat)o).min())) {
615      return true;
616    }
617    if ((o instanceof UpperBoundFloat) && (elts_min > ((UpperBoundFloat)o).max())) {
618      return true;
619    }
620
621    return false;
622  }
623
624  @Override
625  public boolean hasUninterestingConstant() {
626
627    for (int i = 0; i < num_elts; i++) {
628      if (elts[i] < -1.0 || elts[i] > 2.0 || elts[i] != (long)elts[i]) {
629        return true;
630      }
631    }
632
633    return false;
634  }
635
636  @Pure
637  @Override
638  public boolean isExact() {
639    return num_elts == 1;
640  }
641
642  // Look up a previously instantiated invariant.
643  public static @Nullable EltOneOfFloat find(PptSlice ppt) {
644    assert ppt.arity() == 1;
645    for (Invariant inv : ppt.invs) {
646      if (inv instanceof EltOneOfFloat) {
647        return (EltOneOfFloat) inv;
648      }
649    }
650    return null;
651  }
652
653  // Interning is lost when an object is serialized and deserialized.
654  // Manually re-intern any interned fields upon deserialization.
655  private void readObject(ObjectInputStream in) throws IOException,
656    ClassNotFoundException {
657    in.defaultReadObject();
658
659    for (int i = 0; i < num_elts; i++) {
660      elts[i] = Intern.intern(elts[i]);
661    }
662  }
663
664  /**
665   * Merge the invariants in invs to form a new invariant. Each must be a EltOneOfFloat invariant.
666   * This code finds all of the oneof values from each of the invariants and returns the merged
667   * invariant (if any).
668   *
669   * @param invs list of invariants to merge. The invariants must all be of the same type and should
670   *     come from the children of parent_ppt. They should also all be permuted to match the
671   *     variable order in parent_ppt.
672   * @param parent_ppt slice that will contain the new invariant
673   */
674  @Override
675  public @Nullable Invariant merge(List<Invariant> invs, PptSlice parent_ppt) {
676
677    // Create the initial parent invariant from the first child
678    EltOneOfFloat  first = (EltOneOfFloat) invs.get(0);
679    EltOneOfFloat result = first.clone();
680    result.ppt = parent_ppt;
681
682    // Loop through the rest of the child invariants
683    for (int i = 1; i < invs.size(); i++ ) {
684
685      // Get this invariant
686      EltOneOfFloat inv = (EltOneOfFloat) invs.get(i);
687
688      // Loop through each distinct value found in this child and add
689      // it to the parent.  If the invariant is falsified, there is no parent
690      // invariant
691      for (int j = 0; j < inv.num_elts; j++) {
692        double val = inv.elts[j];
693
694        InvariantStatus status = result.add_mod_elem(val, 1);
695        if (status == InvariantStatus.FALSIFIED) {
696
697          result.log("%s", "child value '" + val + "' destroyed oneof");
698
699          return null;
700        }
701      }
702    }
703
704    result.log("Merged '%s' from %s child invariants", result.format(), invs.size());
705    return result;
706  }
707
708  /**
709   * Setup the invariant with the specified elements. Normally used when searching for a specified
710   * OneOf. The elements of vals are not necessarily interned; this method interns each element.
711   */
712  public void set_one_of_val(double[] vals) {
713
714    num_elts = vals.length;
715    for (int i = 0; i < num_elts; i++) {
716      elts[i] = Intern.intern(vals[i]);
717    }
718  }
719
720  /**
721   * Returns true if every element in this invariant is contained in the specified state. For
722   * example if x = 1 and the state contains 1 and 2, true will be returned.
723   */
724  @Override
725  public boolean state_match(Object state) {
726
727    if (num_elts == 0) {
728      return false;
729    }
730
731    if (!(state instanceof double[])) {
732      // Daikon is about to crash.  Produce some debugging output.
733      System.out.printf("state = %s [%s]%n", state, state.getClass());
734      System.out.printf("problem with %s%n", this);
735    }
736    double[] e = (double[]) state;
737    for (int i = 0; i < num_elts; i++) {
738      boolean match = false;
739      for (int j = 0; j < e.length; j++) {
740        if (elts[i] == e[j]) {
741          match = true;
742          break;
743        }
744      }
745      if (!match) {
746        return false;
747      }
748    }
749    return true;
750  }
751
752}