Ordered signatures can not have "exactly 0" instances

[edmcman]

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).

[pkriens]

@dnjackson could you comment?

[alcinocunha]

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.

[grayswandyr]

After discussion: just update the documentation.