Spinroot

A forum for Spin users

You are not logged in.

#1 2012-09-26 12:32:40

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

How to deal with exponentials in any model

I need some way to use an exponential in my model. Is this possible. Can anyone please tell me. I am new one. If this SPIN doesn't support then please tell me if anyone know about any other model checking tool which can handle it. Without this the model cannot be accurate.

Offline

#2 2012-09-27 01:49:00

spinroot
forum
Registered: 2010-11-18
Posts: 694
Website

Re: How to deal with exponentials in any model

Spin is not the right tool for analyzing computational problems -- it analyzes process interactions and coordination.
Sounds like you have a computational problem -- if not, can you say more about why the exponential is essential and cannot be abstracted?

Offline

#3 2012-09-27 02:03:44

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Re: How to deal with exponentials in any model

Then can you please help me in analyzing the correct tool wwhich can handle these calculations and better for distributed systems, have real time. Is there any tool of such kind. I need guidance from you.

Offline

#4 2012-09-27 07:29:15

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: How to deal with exponentials in any model

For real-time model checking, please check uppaal.  For complex computations like exponential you may use Matlab or simply a C compiler.

Offline

#5 2012-09-27 16:37:03

MuhammadIsmail
Member
From: Pakistan
Registered: 2012-05-22
Posts: 23

Re: How to deal with exponentials in any model

Can you please tell me whether UPPAAL can deal with arrays, exponentials and distributed systems. SPIN also uses C compiler (cygwin). I think then it should support exponentials. Also tell me whether MATLAB can do formal verification (model checking)

Offline

#6 2012-09-28 10:39:13

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: How to deal with exponentials in any model

UPPAAL has arrays and is suitable for distributed systems, perhaps no exponential.  To have more information please visit uppaal.org.
You can use embedded C code in SPIN and then you may use exponential.
Matlab has a tool box called Simulink Design Verifier, but you need to pay extra money for that.

Offline

Board footer

Powered by FluxBB