what is a spin model checker? reference?
On Wed, Aug 28, 2013 at 12:11 PM, David Blubaugh < [email protected]> wrote: > Has anyone ever used the spin model checker for verifying and validating > designs within TinyOS??? > > Also, can the designs with tinyos be of any large complexity or is there a > limit to the complexity of design??? > how do you define complexity? how do you measure it? tinyos programs are typically limited by RAM and code size. > David Blubaugh > > > > > > > > > *From:* "[email protected]" < > [email protected]> > *To:* [email protected] > *Sent:* Wednesday, August 28, 2013 3:00 PM > *Subject:* Tinyos-help Digest, Vol 124, Issue 26 > > Send Tinyos-help mailing list submissions to > [email protected] > > To subscribe or unsubscribe via the World Wide Web, visit > > https://www.millennium.berkeley.edu/cgi-bin/mailman/listinfo/tinyos-help > > or, via email, send a message with subject or body 'help' to > [email protected] > > You can reach the person managing the list at > [email protected] > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Tinyos-help digest..." > > > Today's Topics: > > 1. LEAP+ Protocol (Syed Abdul basir) > 2. Help:Telosb BaseStation (Nilavra Pathak) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Wed, 28 Aug 2013 04:19:20 -0700 (PDT) > From: Syed Abdul basir <[email protected]> > Subject: [Tinyos-help] LEAP+ Protocol > To: "[email protected]" > <[email protected]> > Message-ID: > <[email protected]> > Content-Type: text/plain; charset="iso-8859-1" > > I am trying to compile leap+ code. getting the following error. can any > one help me thanks.? the red highlightederrors. thanks. > > > > In file included from myLeapAppC.nc:17: > In component `myLeapP': > myLeapP.nc:31: interface MYA not found > In file included from myLeapAppC.nc:17: > myLeapP.nc:55: syntax error before `uint32_t' > myLeapP: `ReceiveHello.receive' not implemented > myLeapP: `TimerLed1Toggle.fired' not implemented > myLeapP: `AMControl.startDone' not implemented > myLeapP: `AMControl.stopDone' not implemented > myLeapP: `TimerTimeStamp.fired' not implemented > myLeapP: `Boot.booted' not implemented > myLeapP: `AMSendTimeStamp.sendDone' not implemented > myLeapP: `TimerHello.fired' not implemented > myLeapP: `ReceiveStart.receive' not implemented > myLeapP: `TimerMsgs.fired' not implemented > myLeapP: `AMSendAck.sendDone' not implemented > myLeapP: `TimerMain.fired' not implemented > myLeapP: `TimerACK.fired' not implemented > myLeapP: `AMSendTimeKeys.sendDone' not implemented > myLeapP: `TimerHelloCount.fired' not implemented > myLeapP: `TimerLed2Toggle.fired' not implemented > myLeapP: `AMSendHello.sendDone' not implemented > myLeapP: `TimeTimeKeys.fired' not implemented > myLeapP: `ReceiveAck.receive' not implemented > myLeapP: `TimerLed0Toggle.fired' not implemented > In file included from > /opt/tinyos-2.1.0/tos/chips/cc2420/packet/sim/CC2420PacketC.nc:25, > ???????????????? from > /opt/tinyos-2.1.0/tos/chips/cc2420/csma/sim/CC2420CsmaC.nc:16, > ???????????????? from > /opt/tinyos-2.1.0/tos/chips/cc2420/sim/CC2420RadioC.nc:63, > ???????????????? from > /opt/tinyos-2.1.0/tos/chips/cc2420/sim/CC2420ActiveMessageC.nc:75, > ???????????????? from > /opt/tinyos-2.1.0/tos/platforms/micaz/sim/ActiveMessageC.nc:61, > ???????????????? from myLeapAppC.nc:18: > In component `CC2420PacketP': > /opt/tinyos-2.1.0/tos/chips/cc2420/packet/sim/CC2420PacketP.nc: In > function `getNetwork': > /opt/tinyos-2.1.0/tos/chips/cc2420/packet/sim/CC2420PacketP.nc:66: > warning: initialization from incompatible pointer type > /opt/tinyos-2.1.0/tos/chips/cc2420/lpl/DummyLplC.nc:39:2: warning: > #warning "*** LOW POWER COMMUNICATIONS DISABLED ***" > make: *** [sim-exe] Error 1 > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: > https://www.millennium.berkeley.edu/pipermail/tinyos-help/attachments/20130828/fdb9aaad/attachment-0001.htm > > ------------------------------ > > Message: 2 > Date: Wed, 28 Aug 2013 09:04:38 -0400 > From: Nilavra Pathak <[email protected]> > Subject: [Tinyos-help] Help:Telosb BaseStation > To: [email protected], > [email protected] > Message-ID: > <CADfuJwKQtSSK==h2a_dFkRwHbpTAmaPpH7=5pwujihyvo30...@mail.gmail.com> > Content-Type: text/plain; charset="iso-8859-1" > > Hey Guys, > > I have tried to make the BaseStation program run in the Telosb mote. I am > using Ubuntu 13.04 for this . > > But every-time I try running the program nothing happens. > > To test whether the mote is working or not I have run the Blink program and > it worked perfectly well . > > So help please. > > -Nilavra. > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: > https://www.millennium.berkeley.edu/pipermail/tinyos-help/attachments/20130828/c3c09c20/attachment-0001.htm > > ------------------------------ > > _______________________________________________ > Tinyos-help mailing list > [email protected] > https://www.millennium.berkeley.edu/cgi-bin/mailman/listinfo/tinyos-help > > End of Tinyos-help Digest, Vol 124, Issue 26 > ******************************************** > > > > _______________________________________________ > Tinyos-help mailing list > [email protected] > https://www.millennium.berkeley.edu/cgi-bin/mailman/listinfo/tinyos-help > -- Eric B. Decker Senior (over 50 :-) Researcher
_______________________________________________ Tinyos-help mailing list [email protected] https://www.millennium.berkeley.edu/cgi-bin/mailman/listinfo/tinyos-help
