You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
module Foo
// Uncommenting the following line results in no instance being found
open util/ordering[ZeroSig]
sig ZeroSig {}
// Sat
run {} for 3 but exactly 1 ZeroSig
// Unsat
run {} for 3 but exactly 0 ZeroSig
This is affecting me because I have an ordered Sig that I occasionally need to be empty (i.e., exactly 0).
The text was updated successfully, but these errors were encountered:
The ordering module uses directly the total order definition from Kodkod, which requires that at least one element exists: first and last are always defined. We could have a different implementation of the ordering module that allowed empty sigs, but then we could not rely directly on the Kodkod implementation, and we would loose on efficiency. Maybe we need to add a note to the documentation of the module clarifying that the scope must be at least 1.
This is affecting me because I have an ordered Sig that I occasionally need to be empty (i.e., exactly 0).
The text was updated successfully, but these errors were encountered: