Re: [tlaplus] tlc is throwing a classcastexception.

[Paulo Feodrippe]

Hi Avi,

You are not setting the next value of `channel`, try `Next == channel' = Filter2(channel)` and let us know how it goes o/

See ya

Em ter., 20 de abr. de 2021 às 21:36, Avi Feygin <ariel...@gmail.com> escreveu:

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8fe6ac84-62ac-426a-8200-9bdcc50688bbn%40googlegroups.com.

--

Paulo Rafael Feodrippe,

Desenvolvedor

[Markus Kuppe]

On 20.04.21 17:36, Avi Feygin wrote:
> 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')

Hi Avi,

please disable profiling on the "TLC Options" page of the Toolbox model
to avoid the ClassCastException.

Markus