Requirement evaluation ignores assume constraints (assumption false is reported as violated)

Đã đóng
  • Có gì không ổn?
#1,776 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

Một pull request liên quan đã được merge.

  • #1791 của @devin-ai-integration — đã merge

Đánh giá

Độ khó
3/5
Thời gian dự kiến
1-2 ngày
Mức phù hợp với người mới
55/100
Loại issue
Lỗi
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Sôi nổi
Công nghệ
go
Lĩnh vực
compilers

Hướng nghiên cứu

The bug is in the Go code that evaluates requirement checks; find the function implementing RequirementConstraintCheck or the satisfy command (likely in a requirements or evaluation package). Run sysml assume.sysml -satisfy to reproduce the wrong violations. Done when satisfy levelOk by off reports hold and by on reports fail.

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

Mô tả

Summary

When a requirement has an assume constraint, OpenSysML evaluates only the required constraints and ignores the assumptions. A subject for which the assumption is false is reported as violating the requirement.

The standard library defines the result of a requirement check as (Requirements.sysml, RequirementConstraintCheck):

return result = allTrue(assumptions()) implies allTrue(constraints())

so when an assumption is false the requirement holds.

Reproduction

assume.sysml:

package Repro {
    private import ScalarValues::*;
    part def Thing { attribute enabled : Boolean; attribute level : Integer; }
    requirement def LevelOk {
        subject t : Thing;
        assume constraint { t.enabled }
        require constraint { t.level == 1 }
    }
    // assumption false -> by RequirementConstraintCheck::result, LevelOk should hold
    part off : Thing { attribute :>> enabled = false; attribute :>> level = 5; }
    // assumption true, required constraint false -> LevelOk should fail
    part on : Thing { attribute :>> enabled = true; attribute :>> level = 5; }
    requirement levelOk : LevelOk;
    satisfy levelOk by off;
    satisfy levelOk by on;
}

$ sysml assume.sysml -satisfy
✓ package Repro
✗ satisfy levelOk by off fails (on Repro::off ID: 1)
  Required condition evaluated to false: t.level == 1
  standing: violated (witnessed: 1 run under reverse)
✗ satisfy levelOk by on fails (on Repro::on ID: 2)
  Required condition evaluated to false: t.level == 1
  standing: violated (witnessed: 1 run under reverse)

The REPL gives the same result:

%instantiate Repro::off
%requirement Repro::LevelOk off
✗ Requirement Repro::LevelOk failed (on Repro::off ID: 1)
  Required condition evaluated to false: t.level == 1
Expected
  • satisfy levelOk by off holds (assumption t.enabled is false).
  • satisfy levelOk by on fails (assumption true, t.level == 1 false).
Version

Reproduced on linux-amd64 with:

  • sysml v0.11.0 (commit ddf4df00037d6ddbfb1fa9d743a4389f75c9e2dc), the latest release
  • sysml v0.10.0 (commit 08ef397841767b829e492bbecf6d723483b4421e)
Ngôn ngữ chính
Go
Star
47
Fork
13
Merge trung bình
15 giờ 10 phút
Pull request đã merge (30 ngày)
930

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.