feat(verify): bind the in parameters of a constraint or requirement at check time

api/proto/sysml.proto

@@ -241,6 +241,13 @@ message VerifyConstraintRequest {
   // solver questions are reported as the "verification_questions" capability
   // and need an SMT solver.
   string question = 5;
+  // Values for the constraint's `in` parameters, in declaration order, as
+  // RunAnalysisRequest.arguments binds a case's; an argument the constraint
+  // does not take is INVALID_ARGUMENT, as is a parameter left without an
+  // argument or default. Reported as the "verification_arguments" capability.
+  repeated Value arguments = 6;
+  // Values for `in` parameters by name; see arguments.
+  map<string, Value> named_arguments = 7;
 }
 
 // VerifyConstraintResponse carries the verdict; its engine, strength and bounds
@@ -269,6 +276,11 @@ message VerifyRequirementRequest {
   string engine = 4;
   // The question asked; see VerifyConstraintRequest.question.
   string question = 5;
+  // Values for the requirement's `in` parameters, positional and by name; see
+  // VerifyConstraintRequest.arguments. Reported as the "verification_arguments"
+  // capability.
+  repeated Value arguments = 6;
+  map<string, Value> named_arguments = 7;
 }
 
 // VerificationVerdict is what the body of a verification case answered when it

changes/unreleased/verify-arguments.added.md

@@ -0,0 +1 @@
+- **A constraint or requirement with `in` parameters is verified with arguments for them.** `VerifyConstraint` and `VerifyRequirement` take `arguments`, bound positionally in declaration order, and `named_arguments`, bound by name, as `RunAnalysis` binds a case's inputs; a name no parameter has, more positional values than parameters, a parameter left without a value, default or same-named value on the checked object, or a value not of the parameter's type is an undecided verdict naming it, and the symbolic `holds` and `satisfiable` questions refuse them. The service advertises the `verification_arguments` capability; every client binds them (`VerifyArguments`/`VerifyArgument` in Go, `arguments=`/`named_arguments=` in Python, Julia and MATLAB, `VerifyOptions` in Node, Rust and Java). `%constraint`, `%requirement`, `-constraint` and `-requirement` take them in parentheses after the name, with an object as the subject after them, as `%analysis` does: `%requirement Pkg::Under(limit = 5) Pkg::part`.

client/java/opensysml-client/src/main/java/org/openmbee/opensysml/Capabilities.java

@@ -30,6 +30,9 @@ public final class Capabilities {
   /** The verification RPCs answer {@code holds} and {@code satisfiable} questions, reporting a verdict's status and witness. */
   public static final String VERIFICATION_QUESTIONS = "verification_questions";
 
+  /** {@code VerifyConstraint} and {@code VerifyRequirement} bind {@code arguments} and {@code named_arguments} to the element's {@code in} parameters. */
+  public static final String VERIFICATION_ARGUMENTS = "verification_arguments";
+
   /** An analysis response carries each call the run made to a calc held as a value, such as a trade study's evaluation of every alternative. */
   public static final String CASE_EVALUATIONS = "case_evaluations";
 

client/java/opensysml-client/src/main/java/org/openmbee/opensysml/Model.java

@@ -855,8 +855,13 @@ private Verification verifyConstraint(
     Objects.requireNonNull(symbolId, NAME_SYMBOL_ID);
     connection.capabilities().require(Capabilities.VERIFICATION);
     requireQuestion(options);
+    requireArguments(options);
     VerifyConstraintRequest.Builder request =
-        VerifyConstraintRequest.newBuilder().setModelHash(hash).setSymbolId(symbolId);
+        VerifyConstraintRequest.newBuilder()
+            .setModelHash(hash)
+            .setSymbolId(symbolId)
+            .addAllArguments(Protos.protos(options.arguments(), connection.capabilities()))
+            .putAllNamedArguments(Protos.protos(options.namedArguments(), connection.capabilities()));
     subjectSymbolId.ifPresent(request::setSubjectSymbolId);
     engine.ifPresent(request::setEngine);
     questionField(options).ifPresent(request::setQuestion);
@@ -937,8 +942,13 @@ private Verification verifyRequirement(
     Objects.requireNonNull(symbolId, NAME_SYMBOL_ID);
     connection.capabilities().require(Capabilities.VERIFICATION);
     requireQuestion(options);
+    requireArguments(options);
     VerifyRequirementRequest.Builder request =
-        VerifyRequirementRequest.newBuilder().setModelHash(hash).setSymbolId(symbolId);
+        VerifyRequirementRequest.newBuilder()
+            .setModelHash(hash)
+            .setSymbolId(symbolId)
+            .addAllArguments(Protos.protos(options.arguments(), connection.capabilities()))
+            .putAllNamedArguments(Protos.protos(options.namedArguments(), connection.capabilities()));
     subjectSymbolId.ifPresent(request::setSubjectSymbolId);
     engine.ifPresent(request::setEngine);
     questionField(options).ifPresent(request::setQuestion);
@@ -1741,6 +1751,13 @@ private static Optional<String> questionField(VerifyOptions options) {
     return Optional.of(options.question());
   }
 
+  // Refuse to send bindings a service without verification_arguments would silently drop.
+  private void requireArguments(VerifyOptions options) {
+    if (options.bindsArguments()) {
+      connection.capabilities().require(Capabilities.VERIFICATION_ARGUMENTS);
+    }
+  }
+
   // Refuse to send a question a service without verification_questions would evaluate instead.
   private void requireQuestion(VerifyOptions options) {
     questionField(options)

client/java/opensysml-client/src/main/java/org/openmbee/opensysml/VerifyOptions.java

@@ -1,15 +1,25 @@
 package org.openmbee.opensysml;
 
+import java.util.Collections;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
 import java.util.Objects;
 
 /**
- * The question a verification asks: an evaluation of the declared or held values (the default), or
- * a {@code holds} or {@code satisfiable} question the service's solvers answer — a question other
- * than {@link #QUESTION_EVALUATE} needs {@code verification_questions}.
+ * What a verification asks and the values it asks it over: an evaluation of the declared or held
+ * values (the default), or a {@code holds} or {@code satisfiable} question the service's solvers
+ * answer — a question other than {@link #QUESTION_EVALUATE} needs {@code verification_questions}.
+ * The arguments bind the constraint's or requirement's {@code in} parameters, positionally in
+ * declaration order or by name; any binding needs {@code verification_arguments} and only an
+ * evaluation accepts one, since a solver question decides those values itself.
  *
  * @param question the question, as the service spells it
+ * @param arguments values binding the {@code in} parameters in declaration order
+ * @param namedArguments values binding {@code in} parameters by name
  */
-public record VerifyOptions(String question) {
+public record VerifyOptions(
+    String question, List<Value> arguments, Map<String, Value> namedArguments) {
 
   /** The evaluation a verification asks unless a question names another. */
   public static final String QUESTION_EVALUATE = "evaluate";
@@ -21,31 +31,84 @@ public record VerifyOptions(String question) {
   public static final String QUESTION_SATISFIABLE = "satisfiable";
 
   /**
-   * Creates options asking a question.
+   * Creates options, copying the argument collections.
    *
-   * @param question the question, never {@code null}
+   * @param question the question
+   * @param arguments the positional arguments
+   * @param namedArguments the named arguments
    */
   public VerifyOptions {
     Objects.requireNonNull(question, "question");
+    Objects.requireNonNull(arguments, "arguments");
+    Objects.requireNonNull(namedArguments, "namedArguments");
+    arguments = List.copyOf(arguments);
+    namedArguments = Collections.unmodifiableMap(new LinkedHashMap<>(namedArguments));
   }
 
   /**
-   * The default options: an evaluation.
+   * Creates options asking a question with no arguments.
    *
-   * @return options asking {@link #QUESTION_EVALUATE}
+   * @param question the question
+   */
+  public VerifyOptions(String question) {
+    this(question, List.of(), Map.of());
+  }
+
+  /**
+   * The evaluation, with no arguments.
+   *
+   * @return the default options
    */
   public static VerifyOptions defaults() {
     return new VerifyOptions(QUESTION_EVALUATE);
   }
 
   /**
-   * Options asking one question.
+   * Creates options asking a question.
    *
-   * @param question the question: one of {@link #QUESTION_EVALUATE}, {@link #QUESTION_HOLDS} or
-   *     {@link #QUESTION_SATISFIABLE}
-   * @return options asking it
+   * @param question the question, as the service spells it
+   * @return the options
    */
   public static VerifyOptions asking(String question) {
     return new VerifyOptions(question);
   }
+
+  /**
+   * The same options with these positional arguments.
+   *
+   * @param arguments the arguments, in parameter order
+   * @return the options
+   */
+  public VerifyOptions withArguments(List<Value> arguments) {
+    return new VerifyOptions(question, arguments, namedArguments);
+  }
+
+  /**
+   * The same options with these positional arguments.
+   *
+   * @param arguments the arguments, in parameter order
+   * @return the options
+   */
+  public VerifyOptions withArguments(Value... arguments) {
+    return withArguments(List.of(arguments));
+  }
+
+  /**
+   * The same options with these named arguments.
+   *
+   * @param namedArguments the arguments by parameter name
+   * @return the options
+   */
+  public VerifyOptions withNamedArguments(Map<String, Value> namedArguments) {
+    return new VerifyOptions(question, arguments, namedArguments);
+  }
+
+  /**
+   * Whether any argument is bound.
+   *
+   * @return true when a positional or named argument is present
+   */
+  public boolean bindsArguments() {
+    return !arguments.isEmpty() || !namedArguments.isEmpty();
+  }
 }