Should util/boolean use a private function?

[hwayne]

In utils/boolean we have

fun subset_[s1, s2: set Bool] : Bool {
  (s1 in s2) => True else False
}

I think subset_ is supposed to be private to the module. I think boolean was written before Alloy 4, which added the private keyword.

[pkriens]

I think this could use an overhaul anyway. I think using an enum would be nice and I'd like more methods that return the primitive boolean. We could then also add test cases. For example

module util/boolean

enum  Bool { True, False }

pred Bool.isTrue            { this in True }
pred Bool.isFalse           { this in False }

fun Bool.Not : Bool                     { Bool - this }
pred Bool.NOT                       { this = False }

fun Bool.And[b: Bool] : Bool        { subset_[this + b, True] }
pred AND[b: set Bool]           { b in True }

fun Bool.Or [b: Bool] : Bool        { subset_[True, this + b] }
pred OR[b : set Bool]                   { some b & True }

fun Bool.Xor[b: Bool] : Bool        { subset_[Bool, this + b] }
pred XOR[b : set Bool]                  { b = Bool }

fun Bool.Nand[b: Bool] : Bool       { subset_[False, this + b]}
pred NAND[b : set Bool]             { not ( b in True ) }

fun Bool.Nor[b: Bool] : Bool        { subset_[this+ b, False] }
pred NOR[b: set Bool]           { not ( some b & True ) }

private fun subset_[s1, s2: set Bool] : Bool {
  (s1 in s2) => True else False
}

check orGate {

    { a, b, out : Bool | out.isTrue iff OR[a+b] } =  
        False -> False -> False +
        False -> True  -> True +
        True  -> True  -> True +
        True  -> False -> True
}
check orGate {
    { a, b, out : Bool | a.Or[b] = out }  =
        False -> False -> False +
        False -> True  -> True +
        True  -> True  -> True +
        True  -> False -> True
}

check xorGate {

    { a, b, out : Bool | out.isTrue iff XOR[a+b] } =  
        False -> False -> False +
        False -> True  -> True +
        True  -> True  -> False +
        True  -> False -> True
}
check xorGate {
    { a, b, out : Bool | a.Or[b] = out }  =
        False -> False -> False +
        False -> True  -> True +
        True  -> True  -> True +
        True  -> False -> True
}
check andGate {

    { a, b, out : Bool | out.isTrue iff AND[a+b] } =  
        False -> False -> False +
        False -> True  -> False +
        True  -> True  -> True +
        True  -> False -> False
}
check andGate {
    { a, b, out : Bool | a.And[b] = out }  =
        False -> False -> False +
        False -> True  -> False +
        True  -> True  -> True +
        True  -> False -> False
}

check nandGate {
    all a, b : Bool {
        AND[a+b] iff not NAND[a+b]
        a.And[b].Not = a.Nand[b]
    }
}
check norGate {
    all a, b : Bool {
        OR[a+b] iff not NOR[a+b]
        a.Or[b].Not = a.Nor[b]
    }
}

check notGate {
    { a, out : Bool | out=a.Not } = False->True + True->False
}

[aleksandarmilicevic]

In utils/boolean we have

fun subset_[s1, s2: set Bool] : Bool {
  (s1 in s2) => True else False
}

I think subset_ is supposed to be private to the module. I think boolean was written before Alloy 4, which added the private keyword.

Yes, it should be a private function.