microsoft / microsoft/pict

Illegal combination given when o:1 set

Open
#40 4 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
C++
Stars
1.5k
Forks
323
Avg merge
2h 5m
Merged PRs (30d)
4

Description

Hi Jacek,

I seem to be getting an illegal output but only when I've got the order set to 1 (version 3.3.8.0).

Here is my model file:
CCC: H, L
A0: 0,1
A1: 0,1
B0: 0,1
B1: 0,1
L0: 0,1
L1: 0,1
BIG: 0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32

IF [CCC] IN {"H"} THEN
([A0] = 1 OR [A1] = 1) AND ([B0] = 1 OR [B1] = 1);

IF [CCC] IN {"L"} THEN
[L0] = 1 OR
[L1] = 1;

If I run with /o:1 then I end up with cases where "CCC" is "H" and both A0 and A1 are 0.

If I run with /o:2 or above I don't get this issue.

I thought I'd let you know in case there is a bug in the tool or incase I'm doing something wrong.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Reproduce the reported model with the tool's /o:1 option, then compare its cases with runs using /o:2 or higher. Verify whether /o:1 produces a case where CCC is H while both A0 and A1 are 0; done means determining whether that output violates the stated constraint and documenting or correcting the behavior.

Written by the indexing model from the issue text.

Assessment

Tech stack
cpp
Domain
testing-qa
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.