CODEWITHSUNDEEP
state-machinealloy
roll
roll

Reputation: 125

Writing a Finite state machine specification in Alloy

I m new in alloy. I am triying to make analog phone line specs in allow. Here is my FSM diagram. FSM visio diagram

I have written a sample code to illustrate state transition.My transsition table is a fact, however output multiplicy is a problem in alloy syntax. I cant run this code.

Would you say me what is wrong. And any suggestion?

module state
sig Input{}
abstract sig State {
transition:  Input-> State-> Output}
one sig  NULL extends State {}
one sig CALL_RECEIVED extends State {}
fact xTable {
NULL->one setup_ind :Input->CALL_RECEIVED->one alerting_req:Output in transition
CALL_RECEIVED->one disconnect_ind:Input->NULL->one clear: Output in transition
}
pred show {}
run show

Upvotes: 2

Views: 1767

Answers (1)

Aleksandar Milicevic
Aleksandar Milicevic

Reputation: 3867

The problem is that you are using a made up syntax inside the xTable fact. I suggest you look at http://alloy.mit.edu/alloy/documentation.html and learn the Alloy basics first.

Upvotes: 3

Related Questions