Scott Lystig Fritchie
b3ed9ef51c
Add fill checking to PULSE model, minimal API coverage is complete
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
7a46709c13
Change transition type names to make better invalid transition detection
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
8a56771182
Add better condition for perhaps_trip_fill_page()
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
db6fa3d895
Fix two bugs found by PULSE in corfurl_flu.erl, yay!
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
86d4583aef
Add fill support to the PULSE model
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
7dba8beae9
Refactor PULSE test for easier checking, prior to adding fill & trim.
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
78019b402f
Refactor the PULSE model testing error 'trip' code
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
c80921de25
Add scan_forward() command, no result checking yet
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
fb6b1cdc3c
Fix read_page() model problem: no more false positives!
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
e9851767fc
Add read_page() temporal check
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
a7aff2f141
Dumbdumbdumb don't interfere with event_logger:event() duh!
2015-03-02 18:03:09 +09:00
Scott Lystig Fritchie
c14e1facf4
Add read_approx() to the PULSE model, only 5% correctness checks done
2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
572d1803d0
Add (mostly) temporal logic checking for exactly-once append_page().
...
Also, for peace of mind (I hope), I've added this -ifndef to introduce
a bug that should cause the new exactly-once append_page() check to fail.
This should make it easier to change the model and *TEST* the changes,
to avoid breaking the model without ever knowing it.
2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
25bf64a03c
Just in case commit: WIP
2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
58ced8d14c
Add PULSE control over sequencer handing out duplicate page numbers
2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
21a3fd6d07
Use temporal logic for check_trace()
2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
e0ec95e8f7
Added small PULSE usage sketch in docs/corfurl.md
2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
b430fa479c
PULSE condition checking is only 98% embarassing
2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
bcc6cf1e6a
PULSE bugfix: race with finish_init message
2015-03-02 18:03:08 +09:00
Scott Lystig Fritchie
a294a0eff0
Skeleton of PULSE test created, first bug (race in sequencer init) is found, huzzah!
2015-03-02 18:03:05 +09:00
Scott Lystig Fritchie
feed231d5e
Move EUnit test code to test subdir
2015-03-02 17:59:31 +09:00
Scott Lystig Fritchie
3963ce44f0
More sanity checking for fill() in smoke test
2015-03-02 17:57:31 +09:00
Scott Lystig Fritchie
3d2be7255f
Basic smoke test for read repair
2015-03-02 17:57:31 +09:00
Scott Lystig Fritchie
6014b0584e
Fix read() response to a prior fill
2015-03-02 17:57:31 +09:00
Scott Lystig Fritchie
c23aeabc20
Read-repair, not tested
2015-03-02 17:57:30 +09:00
Scott Lystig Fritchie
945635f837
Basic scan_forward done
2015-03-02 17:57:30 +09:00
Scott Lystig Fritchie
05a71eebb0
corfurl:read_page() done, no read-repair yet
2015-03-02 17:57:30 +09:00
Scott Lystig Fritchie
72bf329e1c
Add fledgling log implementation based on CORFU papers
2015-03-02 17:57:27 +09:00
