Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

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

Đang mở
  • Có gì không ổn?
#719 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

Maintainer thường phản hồi trong vòng 1 ngày

Chưa có ai nhận issue này.

Đánh giá

Độ khó
5/5
Thời gian dự kiến
Hơn một tuần
Mức phù hợp với người mới
35/100
Loại issue
Tính năng
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Sôi nổi
Công nghệ
go
Lĩnh vực
backend

Hướng nghiên cứu

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.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

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.

Ngôn ngữ chính
Go
Star
24
Fork
5
Merge trung bình
10 giờ 11 phút
Pull request đã merge (30 ngày)
572

Chuẩn bị môi trường

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của Open-MBEE/OpenSysML

Tất cả issue của Open-MBEE/OpenSysML

Issue tương tự

Thêm issue về Go

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.