Hacktoberfest 2026: los issues que los mantenedores marcaron para octubre, abiertos y aptos para principiantes. Explorar issues de Hacktoberfest

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

Abierto
  • ¿Algo no está bien?
#719 0 comentarios 0 reacciones 0 asignados Ver en GitHub

Los mantenedores suelen responder en 1 día

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
5/5
Tiempo estimado
Más de una semana
Aptitud para principiantes
35/100
Tipo de issue
Nueva funcionalidad
Claridad
Bastante claro
Estado de actividad
Activo
Stack tecnológico
go
Área
backend

Línea de trabajo

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.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

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.

Lenguaje dominante
Go
Estrellas
24
Forks
5
Merge medio
10 h 11 min
PR fusionados (30 d)
572

Preparar el entorno

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de Open-MBEE/OpenSysML

Todos los issues de Open-MBEE/OpenSysML

Issues similares

Más issues de Go

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.