diff --git a/Src/PChecker/CheckerCore/PRuntime/Values/PrtSet.cs b/Src/PChecker/CheckerCore/PRuntime/Values/PrtSet.cs index 6d5c3ff27..474dc47c4 100644 --- a/Src/PChecker/CheckerCore/PRuntime/Values/PrtSet.cs +++ b/Src/PChecker/CheckerCore/PRuntime/Values/PrtSet.cs @@ -37,6 +37,19 @@ private bool IsDirty } } + public override int GetHashCode() + { + if (!IsDirty) + { + return hashCode; + } + + hashCode = ComputeHashCode(); + IsDirty = false; + + return hashCode; + } + public IEnumerator GetEnumerator() { return set.GetEnumerator(); diff --git a/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java b/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java index 064f0403b..b32e5934a 100644 --- a/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java +++ b/Src/PRuntimes/PSymRuntime/src/test/java/psym/TestSymbolicRegression.java @@ -68,6 +68,9 @@ private static void setRunArgs() { } private static void createExcludeList() { + // TODO: fix key not found error when using set as key + excluded.add("../../../Tst/RegressionTests/Integration/Correct/TestMapSet"); + // TODO Unsupported: too many choices to throw error if choices more than 10000 excluded.add("../../../Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSeq"); excluded.add("../../../Tst/RegressionTests/Feature3Exprs/DynamicError/tooManyChoicesSet"); diff --git a/Tst/RegressionTests/Integration/Correct/TestMapSet/TestMapSet.p b/Tst/RegressionTests/Integration/Correct/TestMapSet/TestMapSet.p new file mode 100644 index 000000000..6bbddd8a4 --- /dev/null +++ b/Tst/RegressionTests/Integration/Correct/TestMapSet/TestMapSet.p @@ -0,0 +1,25 @@ + // Recreating set in map error + +machine Main +{ + start state Init { + entry { + ReplicateMapSet(); + } + } +} + +fun ReplicateMapSet() +{ + var seqmap: map[seq[int], int]; // Creating example for comparison + var mapmap: map[map[int, int], int]; + var setmap: map[set[int], int]; + + seqmap[default(seq[int])] = 0; + mapmap[default(map[int,int])] = 1; + setmap[default(set[int])] = 2; + + print format("seqmap: {0}", seqmap[default(seq[int])]); + print format("mapmap: {0}", mapmap[default(map[int,int])]); + print format("setmap: {0}", setmap[default(set[int])]); +}