Why <> Evaluates Negation but Skips Conjunction at Step 0"

[squickly1]

This question was originally posted by LEARN TAU:

At step 0, r <> o1[t] = i1[t]’ performs negation once then o1=0 all the time but r <>o1[t] = i1[t] & i2[t] doesn’t perform "&" operator at step 0. Why? Thank you for your guidance!

[castrod]

How sometimes is Implemented

For each sometimes psi, Tau creates an eventual flag _e0 (satisfiability.tmpl.h:769–798):

_e0[start_time] != 0               ← flag must be non-zero initially
_e0[t-1] = 0 → _e0[t] = 0         ← once zero, stays zero
(_e0[t-1] != 0 && _e0[t] == 0) → (guard → psi)   ← formula fires at transition
sometimes: _e0[t] = 0              ← flag must eventually become zero

A guard (satisfiability.tmpl.h:696–711) wraps every input variable with an uninterpreted constant:

guard = (i1[t] = _uc_i1)                           ← for negation
guard = (i1[t] = _uc_i1) && (i2[t] = _uc_i2)      ← for AND

The full constraint reads: "when the flag fires, IF the inputs equal the chosen constants, THEN the formula holds."

The values of _uc_i1, _uc_i2 are chosen by the synthesis solver — typically the lexicographically minimal satisfying assignment, i.e. all-zero.

---

Why Negation Fires Visibly and AND Does Not

	sometimes o1[t] = i1[t]'	sometimes o1[t] = i1[t] & i2[t]
Constants chosen by solver	_uc_i1 = 0	_uc_i1 = 0, _uc_i2 = 0
Guard fires when	i1[t] = 0	i1[t] = 0 AND i2[t] = 0
Output at firing step	o1 = 0' = T (non-zero, visible)	o1 = 0 & 0 = 0 (zero, invisible)
Output for any other input	0 (guard not matched)	0 (guard not matched)

Providing T, T as inputs still gives F because:

guard = (T = F) && (T = F) = FALSE

The implication FALSE → psi is vacuously true — no constraint on o1, so it defaults to 0.

---

Root Cause

The synthesis found a degenerate but technically valid witness for sometimes (o1 = i1 & i2):

• Guard constants (0, 0) → formula "holds" when inputs are both zero
• 0 & 0 = 0 → output is zero, indistinguishable from o1 not being computed

For negation, the same minimal-constant choice (0) produces F' = T — visible and non-trivial.

The synthesized program for sometimes (o1 = i1 & i2) always outputs 0 because:

1. When inputs are (0, 0): guard fires, AND gives 0
2. When inputs are anything else: guard doesn't fire, o1 = 0

---