Commit Graph

728 Commits

Author SHA1 Message Date
Michael Walker
ce7b0fc9ec Advanced Usage 2017-08-19 16:38:39 +01:00
Michael Walker
a9a6689334 Refinement Testing 2017-08-19 16:38:39 +01:00
Michael Walker
d53b689c5b Unit Testing 2017-08-19 16:38:39 +01:00
Michael Walker
581ab8339a Typeclasses 2017-08-19 16:38:39 +01:00
Michael Walker
c06c32e790 Getting Started 2017-08-19 16:38:39 +01:00
Michael Walker
2b92208947 Sections and headings 2017-08-19 16:38:39 +01:00
Michael Walker
ec68d34e14 Initial commit for sphinx docs 2017-08-19 16:38:39 +01:00
Michael Walker
b39200ab7e Test case doesn't actually need three preemptions 2017-08-19 15:43:21 +01:00
Michael Walker
2a15549d97 Release 2017-08-16 11:26:04 +01:00
Michael Walker
1ec7a37671 Fix dpor/bpor variable naming inconsistency 2017-08-14 14:09:55 +01:00
Michael Walker
d3f6ff1b27 Remove unused dporAction field 2017-08-13 20:29:23 +01:00
Michael Walker
04bc5158fa Force evaluation of DPOR state
This prevents a huge leak.
2017-08-12 11:22:34 +01:00
Michael Walker
235da1e43d Use a stack for the DPOR state
Closes #64
Closes #89
2017-08-12 11:22:34 +01:00
Michael Walker
d68afb4e45 Update Test.DejaFu.Conc.Internal module comment 2017-08-12 11:20:14 +01:00
Michael Walker
07dc91c8fb Remove a bit of boolean blindness 2017-08-12 11:15:50 +01:00
Michael Walker
f53e69dc46 Update Test.DejaFu.Conc.Internal.Memory module comment 2017-08-12 11:10:58 +01:00
Michael Walker
ea2ad13984 Replace some uses of Data.Map.alter with Data.Map.adjust 2017-08-12 11:09:18 +01:00
Michael Walker
746f4c8711 Add a README section about performance 2017-08-11 17:45:52 +01:00
Michael Walker
4d05ef6798 Release 2017-08-10 21:51:11 +01:00
Michael Walker
50712c54cd Merge branch 'discard' 2017-08-10 21:42:30 +01:00
Michael Walker
4e6e9c30fc Fix 'concurrency' version in README 2017-08-10 21:41:20 +01:00
Michael Walker
305cf27c0b Add a test for discarding 2017-08-10 20:22:03 +01:00
Michael Walker
b99caea84c Expose discard functions from Test.Tasty.DejaFu 2017-08-10 16:55:06 +01:00
Michael Walker
3ab42c4936 Expose discard functions from Test.HUnit.DejaFu 2017-08-10 16:45:29 +01:00
Michael Walker
bc0a5e579a Expose the discard logic through Test.DejaFu
New functions: dejafuDiscard and dejafuDiscardIO

No dejafusDiscard and dejafusDiscardIO, because I think the
combination of discarding + sharing traces would be very confusing.
Also, the dejafus* functions are for when you want to trade space for
time, whereas the *Discard* functions are for the opposite.  So it
doesn't make much sense.
2017-08-10 16:45:29 +01:00
Michael Walker
51bad3b5d1 Add a CHANGELOG entry 2017-08-10 16:45:29 +01:00
Michael Walker
100c2d3ab9 Push fmap inside checkDiscard
This seems to improve matters significantly.  Laziness!
2017-08-10 16:45:29 +01:00
Michael Walker
552a0f3816 Add discarding variants of SCT functions
See #90
2017-08-10 16:45:29 +01:00
Michael Walker
2becd6300d Drop use of partial functions in runThreads 2017-08-09 00:00:45 +01:00
Michael Walker
fe9e40747b [travis] Allow nightly build to fail 2017-08-07 22:07:53 +01:00
Michael Walker
a652628fb8 [travis] Only build with latest LTS for each supported GHC version 2017-08-07 22:07:39 +01:00
Michael Walker
325b7e01a3 Factor out continuation running to DejaFu.Common 2017-06-22 09:18:28 +01:00
Michael Walker
b8a039befc Note that semigroups dep of dejafu can be removed with GHC 8.4 2017-06-12 13:49:46 +01:00
Michael Walker
63a3ff73af dejafu-0.7.0.2 release 2017-06-12 03:48:28 +01:00
Michael Walker
0da649dc08 Remove unneeded monad-loops dep 2017-06-12 03:47:04 +01:00
Michael Walker
81ff175f6d Remove some redundant constraints 2017-06-11 23:59:47 +01:00
Michael Walker
9e7e460ab0 Remove a redundant import 2017-06-11 23:57:41 +01:00
Michael Walker
e32f777c32 0.7.0.1 release 2017-06-09 15:15:05 +01:00
Michael Walker
2cc812ddc3 Make checkWithSeeds faster when the result can be inferred early
Often checking every seed is unnecessary to compute the result of
checkWithSeeds.  The first failure always suffices for weak refinement
and equivalence, and sometimes suffices for strict refinement.
2017-06-09 15:14:42 +01:00
Michael Walker
d46319c577 Make checkFor faster when there is only a single counterexample
As mapM in IO is strict, composing listToMaybe with counterExamples
necessitates finding ALL counterexamples first, even though only the
first is returned.  So an improvement is gained by manually making it
"lazy".
2017-06-09 15:14:26 +01:00
Michael Walker
a0a5a493d5 Bump versions for release 2017-06-07 17:09:01 +01:00
Michael Walker
8f27ff0c11 Merge branch 'next-major' 2017-06-07 16:59:40 +01:00
Michael Walker
6bc2fd044f Remove unused imports 2017-06-07 16:59:24 +01:00
Michael Walker
f590f233a8 Implement all nonsense checks directly in the sct* functions 2017-06-07 16:50:56 +01:00
Michael Walker
040580d4f2 Remove bound-specific SCT functions 2017-06-07 16:50:56 +01:00
Michael Walker
6b1fd17024 Implement uniform random scheduling
Adds a new `uniformly` smart constructor and `sctUniformRandom`
function.

Also renames `sctRandom` to `sctWeightedRandom`.
2017-06-07 16:50:56 +01:00
Michael Walker
1146ce9b38 Add a smart constructor for constructing swarmy executions
The `randomly` constructor now corresponds exactly to the old
`Randomly`.

Also refactor tests a bit.
2017-06-07 16:50:56 +01:00
Michael Walker
fba26e6c73 Make Way abstract and expose smart constructors 2017-06-07 16:50:56 +01:00
Michael Walker
d65b8359a9 Allow re-using the weights for multiple executions in sctRandom 2017-06-07 16:45:43 +01:00
Michael Walker
a0698bf575 Merge branch 'propcheck'
Closes #82
2017-06-07 14:32:19 +01:00