Hacktoberfest 2026: le issue che i maintainer hanno segnato per ottobre, aperte e adatte ai principianti. Sfoglia le issue Hacktoberfest

holds/satisfiable: model the evaluator's short-circuit order so an unreadable operand it never reaches does not leave the question undecided

Aperta
  • Qualcosa non va?
#719 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub

I maintainer di solito rispondono entro 1 giorno

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
5/5
Tempo stimato
Più di una settimana
Idoneità per principianti
35/100
Tipo di issue
Funzionalità
Chiarezza
Abbastanza chiara
Stato di attività
Attiva
Stack tecnologico
go
Ambito
backend

Direzione di ricerca

Start in internal/exec/solve/pin.go, where the constraint translation currently treats every named feature as a read, and compare it with the evaluator's left-to-right short-circuit rules. Model undefined terms and operand reachability for and, or, and implies, then add tests covering the true-or-unreadable and free-or-unreadable examples so holds and satisfiable agree with evaluate.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

Behaviour

attribute bad : Real = 1.0 / 0.0;
assert constraint ok { true or bad > 0.0 }

evaluate on ok holds: evalLogical returns on the true left operand of or and never reads bad. holds and satisfiable on the same constraint return undecided, "reads bad, whose value could not be read: division by zero", because the SMT translation treats every feature the expression names as a read.

The answer is conservative, not wrong: no verdict is given rather than a false one. The alternative inside the current translation, leaving bad free, is the unsound behaviour #712 removed (a default that fails to evaluate is no longer a free value).

What an exact answer needs

The translation would have to model the evaluator's left-to-right short-circuit rules: an "undefined" term that propagates through and, or and implies, with reachability that depends on the free values. In free > 0.0 or bad > 0.0, bad is read only where free <= 0.0, so the query has to say so. The operands are not symmetric either: bad > 0.0 or true is undecided under evaluate, while true or bad > 0.0 holds, and the translation must give the same two answers.

This is a change to internal/exec/solve (pin.go, the constraint translation) with its own tests, not part of the fix in https://github.com/Open-MBEE/OpenSysML/pull/712, which keeps the conservative result.

Raised from the review thread https://github.com/Open-MBEE/OpenSysML/pull/712#discussion_r4134833844 on #712.

Lingua principale
Go
Stelle
24
Fork
5
Merge medio
10h 11m
PR unite (30g)
572

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di Open-MBEE/OpenSysML

Tutte le issue di Open-MBEE/OpenSysML

Issue simili

Altre issue su Go

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.