The statement
exists (guarantee : AgreeLib.AgreeGuarantees(c)) . name(guarantee) = spec_name
causes a validation error because it parses AgreeLib.AgreeGuarantees(c) as a LibraryFnType rather than a LibraryFnCall. This means that the QuantifiedExpr arg is parsed as an Arg rather than a QuantArg and causes the validator to complain that only AADL types are supported. In reality AgreeGuarantees() returns a SetExpr, which should be supported.
The statement
exists (guarantee : AgreeLib.AgreeGuarantees(c)) . name(guarantee) = spec_name
causes a validation error because it parses AgreeLib.AgreeGuarantees(c) as a LibraryFnType rather than a LibraryFnCall. This means that the QuantifiedExpr arg is parsed as an Arg rather than a QuantArg and causes the validator to complain that only AADL types are supported. In reality AgreeGuarantees() returns a SetExpr, which should be supported.