package vesta.mc; public abstract class State { abstract public double getTime(); // return the current time of // the state abstract public State duplicate(); // duplicates the current // state and returns it. abstract public void pop(); // just make it an empty function abstract public boolean sat(int i); // sat(i) returns true if the // i-th atomic proposition // holds in the current state abstract public void next(); // computes a next state // of the model from the // current state using // discrete-event simulation // and returns the computed // state public int ival(int i) { // ignore this function throw new AnyException("ival not defined"); } abstract public double rval(int r); // rval(i) returns the value of the // i-th expression in the // current state public long id() { throw new AnyException("Id not defined"); } }VESTA currently provides interfaces for two modelling languages:
vesta2/examples/Tandem.ctmc
and
vesta2/examples/Polling.ctmc
for example.
vesta2/examples/Polling.maude
and
vesta2/examples/tcpsyn.maude
for
example. PMaude
is not distributed with VESTA 2.0. PMaude can be
obtained from here.
P <= 0.05 [<> < 100.0 @0]
: probability that a
message queue eventually becomes full in less than 100 time units is
less than or equal to 0.05. @0
stands for the atomic
proposition full. @0 => (P >= 0.9 [~ @1 U < 5 @2])
: if a
message processing server is rebooted then the probability that it
recovers within 5 time units without dropping any message is greater
than or equal to 0.9. @0
stands for the atomic proposition
reboot, @1
stands for the atomic proposition
drop, and @2
stands for the atomic proposition
recovervesta2/examples/Tandem.csl
and
vesta2/examples/Polling.csl
for example.
CountConnected( ) = if { s.sat(1) } then {s.rval(0)} else
#CountConnected( ) fi ;
eval E[ CountConnected( )] ;
ProbConnected( ) = if { s.getTime( ) > 10.0 } then {0.0} else if { s.sat(0) } then {1.0} else #ProbConnected( ) fi fi ;
eval E[ ProbConnected( ) ];
The syntax of QuaTEx can be found here.
vesta2/examples/Tandem.quatex
and
vesta2/examples/tcpsyn.quatex
for
example.