<jupyter_start><jupyter_text>Some possibly helpful laws:- Posulate 1: ¬( GO ∨ (RES ∧ SEL)) implies all E' is 0 and all kn are 0.- - Correlary 1: This holds for ¬(GO ∨ SEL) - - Correlary 2: This holds for ¬(GO ∨ RES)- Postulate 2: forall n m, m != n, ¬ (kn ^ km), that is at most one k wire is selected.- Postulate 3: SEL can only be 1 if, at some instant in the past GO was 1. (?)<jupyter_code>(define start
  (circuit
   #:inputs (GO Knl K0r Kxr Selr)
   #:outputs (Kn K0 Kx Sel)
  (Knr = GO)
   (Kn = (or Knr Knl))
   (K0 = K0r)
   (Kx = Kxr)
   (Sel = Selr)))
(define end
  (circuit
   #:inputs (GO)
   #:outputs (Kn K0 Kx Sel)
   (Kn = GO)
   (K0 = false)
   (Kx = false)
   (Sel = false)))
(assert-same start end)
(assert-same 
 (compile-esterel (term (seq (exit 0) (nts p 2))))
 (compile-esterel (term (exit 0))))<jupyter_output>assert-same: rosette model gave counterexample:
(model
 [pos-pK0$4 #f]
 [neg-pK0$5 #f]
 [pos-pK1$4 #f]
 [neg-pK1$5 #f]
 [pos-GO$10 #f]
 [neg-GO$11 #f]
 [pos-pK2$4 #f]
 [neg-pK2$5 #f]
 [pos-KILL$4 #f]
 [neg-KILL$5 #f]
 [pos-RES$4 #f]
 [neg-RES$5 #f]
 [pos-SUSP$4 #f]
 [neg-SUSP$5 #f]
 [pos-p-SEL$4 #f]
 [neg-p-SEL$5 #f])
'((((SEL ⊥) (SEL #f))))
'(((pK0 ⊥)
   (pK1 ⊥)
   (GO ⊥)
   (pK2 ⊥)
   (KILL ⊥)
   (RES ⊥)
   (SUSP ⊥)
   (p-SEL ⊥)
   (K0 ⊥)
   (K1 ⊥)
   (K2 ⊥)
   (SEL ⊥)
   (p-GO #f)
   (p-KILL ⊥)
   (p-RES ⊥)
   (p-SUSP ⊥)
   (psel #f)
   (qsel ⊥)))
'(((pK0 ⊥)
   (pK1 ⊥)
   (GO ⊥)
   (pK2 ⊥)
   (KILL ⊥)
   (RES ⊥)
   (SUSP ⊥)
   (p-SEL ⊥)
   (K2 ⊥)
   (SEL #f)))
  context...:
   eval-one-top12
   /Applications/Racket/racket/share/pkgs/sandbox-lib/racket/sandbox.rkt:510:0: call-with-custodian-shutdown
   /Applications/Racket/racket/collects/racket/private/more-scheme.rkt:148:2: call-with-break-parameterization
   .../more-scheme.rkt:261:28
   /Applications/Racket/racket/share/pkgs/sand[...]
{'fraction_non_alphanumeric': 0.20978260869565218, 'fraction_numerical': 0.03641304347826087, 'mean_word_length': 2.734279918864097, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 4, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '1', 'dir': 'jupyter-structured-clean-dedup', 'id': '591879', 'license': 'MIT', 'n_tokens_mistral': 1017, 'n_tokens_neox': 937, 'n_words': 239, 'path': 'circuits/[seq-exit].ipynb', 'repo_name': 'florence/esterel-calculus', 'size': '1840'}