alloy analyzer didn't execute my run command exactly

1
votes

my code is this:

but when I execute this.it show me only one house and one mohre. what should I do???

abstract one sig board{}
sig mohre {live:one  state }
sig house extends board{ver:one Int,hor:one Int,mo: mohre }
enum state{alive,dead}
run{#house>10 and #mohre>8}
1
alloy

1 Answers

2
votes

Your run does not specify a scope. The default scope is 3 atoms of each sig and 16 integers ([-8..7]).

The US of cardinality 10 is therefore out if scope. Basically those models are in lala land. If you lower the cardinality or increase the scope things should work.

   run{#house>10 and #mohre>8} for 12 but 5 int

This command allows 12 atoms of all types and has 32 integers. Weirdly, the integers are specified by their bit width and 5 bits gives you 32 values.

Additionally, you put a constraint on the abstract sig one board. Remove the one since that prevents a solution with more than one house.