we have an assignment to create a basic sieve, and I think I have the theory down
but now it threw this completely unexpected exception.
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.ClassCastException
: class tlc2.tool.coverage.ActionWrapper cannot be cast to class tlc2.tool.coverage.OpApplNodeWrapper (tlc2.tool.coverage.ActionWrapper and tlc2.tool.coverage.OpApplNodeWrapper are in unnamed module of loader 'app')
any advice would be greatly appreciated, as I have no idea even as to the location of the problem as the error has no trace
Below is my spec
------------------------------ MODULE filters ------------------------------
EXTENDS TLC, Sequences, Integers, Naturals
CONSTANTS INPUT(in the model set to <<1,2,3,4,5,6>> ), DIVISORS(in the model set to <<2,3>>
VARIABLE channel
Init == channel = <<INPUT, <<>>, <<>> >>
RECURSIVE Filter(_,_,_)
Filter(a,b,c) == IF (Head(a) # Head(b) /\ Head(a) # <<>>)
THEN <<>>
ELSE IF Head(a) = Head(b) /\ Head(a) # <<>>
THEN Filter(Tail(a), Tail(b), c)
ELSE <<>>
\*RECURSIVE Filter7(_)
\*Filter7(a) == IF Head(channel[1]) # <<>>
\* THEN <<>>
\* ELSE IF (Head(a[1]) % 7 # 0)
\* THEN
\* /\ Filter5(<< Tail(a[1]), (a[2] \o Head(a[1])), <<>> >>)
\* /\ Filter7(<< Tail(a[1]), (a[2] \o Head(a[1])), <<>> >>)
\* ELSE Filter5(<< Tail(a[1]), a[2], <<>> >>)
\*
\*
\*
\*RECURSIVE Filter5(_)
\*Filter5(a) == IF Head(channel[1]) # <<>>
\* THEN <<>>
\* ELSE IF (Head(a[1]) % 5 # 0)
\* THEN
\* /\ Filter5(<< Tail(a[1]), (a[2] \o Head(a[1])), <<>> >>)
\* /\ Filter7(<< Tail(a[1]), (a[2] \o Head(a[1])), <<>> >>)
\* ELSE Filter5(<< Tail(a[1]), a[2], <<>> >>)
RECURSIVE Filter3(_)
Filter3(a) == IF Len(a[2]) > 0
THEN <<>>
\* if head of a[2] is not divisible by 3
ELSE IF (Head(a[2]) % 3 # 0)
THEN
/\ Filter3(<< (Tail(a[1])), (a[2] \o Head(a[1])), a[3] >>)
\* /\ Filter5(<< Tail(a[1]), (a[2] \o Head(a[1])), <<>> >>)
ELSE Filter3(<< (Tail(a[1])), (Tail(a[2])), (a[3] \o Head(a[2])) >>)
RECURSIVE Filter2(_)
\*if head is empty then ignore
Filter2(a) == IF Len(a[1]) > 0
THEN <<>>
\* else if head of << <<!!!>>, <<>>, <<>> >> is not divisible by 2 then
ELSE IF (Head(a[1]) % 2 # 0)
THEN
\* a[1]' = tail(a[1]), a[2]' = a[2] \o head(a[1])
/\ Filter2(<< Tail(a[1]), (a[2] \o Head(a[1])), a[3] >>)
/\ Filter3(<< Tail(a[1]), (a[2] \o Head(a[1])), a[3] >>)
ELSE Filter2(<< Tail(a[1]), a[2], a[3] >>)
Next == Filter2(channel)
=============================================================================
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8fe6ac84-62ac-426a-8200-9bdcc50688bbn%40googlegroups.com.