@Throws(IllegalArgumentException::class) fun ColorPredicate(input: String) { var rest = input.trim { it <= ' ' }.lowercase(Locale.getDefault()) if (rest.startsWith("leaf")) { this.isLeaf = true rest = rest.substring(4).trim { it <= ' ' } } else { this.isLeaf = false } var endOfStartToken = 0 while (endOfStartToken < rest.length && Character.isLetter(rest[endOfStartToken])) { endOfStartToken++ } val startToken = rest.substring(0, endOfStartToken) val macro: String = getMacro(startToken) if (macro != null) { rest = macro } if (rest.startsWith("some")) { this.isSome = true rest = rest.substring(4).trim { it <= ' ' } } else if (rest.startsWith("every")) { this.isSome = false rest = rest.substring(5).trim { it <= ' ' } } else { throw IllegalArgumentException( """ Color predicate must start with the optional keyword `leaf' followed by a legal macro name or `every' or `some'.""" ) } this.set = 0 while (rest != "") { if (rest.startsWith("omitted")) { this.set = this.set or (1 shl NUMBER_OF_OMITTED_STATE) rest = rest.substring(7).trim { it <= ' ' } } else if (rest.startsWith("missing")) { this.set = this.set or (1 shl NUMBER_OF_MISSING_STATE) rest = rest.substring(7).trim { it <= ' ' } } else if (rest.startsWith("(")) { rest = rest.substring(1).trim { it <= ' ' } val stateSetSpec = arrayOfNulls<IntArray>(NUMBER_OF_PROVERS) for (i in 0 until NUMBER_OF_PROVERS) { var invert = falseif (rest.startsWith("-")) { invert = true rest = rest.substring(1).trim { it <= ' ' } } val appears = BooleanArray(PROVER_STATUSES.get(i).length) for (j in appears.indices) { appears[j] = invert } val endChar = if (i == NUMBER_OF_PROVERS - 1) ")" else "," while (rest.length > 0 && !rest.startsWith(endChar)) { var endOfToken = 0 while (endOfToken < rest.length && Character.isLetter(rest[endOfToken])) { endOfToken++ } val token = rest.substring(0, endOfToken) rest = rest.substring(endOfToken).trim { it <= ' ' } var statusNumber: Int try { statusNumber = numberOfProverStatus(i, token) } catch (e: IllegalArgumentException) { val errorMsg = """Was expecting status of prover ${ PROVER_NAMES.get(i).toString() } but found `$token' followed by: `$rest'""" throw IllegalArgumentException(errorMsg) } appears[statusNumber] = !invert } require(rest.length != 0) { "Color predicate specifier ended before `(...)' expression complete" } rest = rest.substring(1).trim { it <= ' ' } var count = 0 for (j in appears.indices) { if (appears[j]) { count++ } }if (count == 0) {require(!invert) { "A `-' must be followed by one or more statuses" } count = appears.size for (j in 0 until count) { appears[j] = true} } stateSetSpec[i] = IntArray(count) var k = 0 for (j in appears.indices) { if (appears[j]) { stateSetSpec[i]!![k] = j k++ } } } this.set = this.set or bitVectorOfStates(stateSetSpec) } else { throw IllegalArgumentException("Unexpected token at: `$rest'") } } }
Returns a ColorPredicate obtained by parsing its argument . See the beginning of ProofStatus.tla for the grammar of the input .