What exactly is the difference between skip and break in PROMELA?

Question

0.00/5 (No votes)

See more:

Let's say I have this piece of PROMELA code

active proctype A(){

   do
      :: !x -> break
      :: else -> skip
   od

   … //more code
}

What exactly does break and skip do in this instance? Does break break out the whole process A() so that "more code" wouldn't be reached or just the loop?

What I have tried:

Researched the net but it still isn't very clear to me.

Posted 3-Dec-18 0:07am

Member 14075527

Updated 3-Dec-18 1:36am

Add a Solution

2 solutions

Add a Solution

Add your solution here

Treat my content as plain text, not as HTML

Preview 0

…

Existing Members

Sign in to your account

...or Join us

Download, Vote, Comment, Publish.

Your Email
Password
Forgot your password?

Your Email
This email is in use. Do you need your password?
Optional Password

I have read and agree to the Terms of Service and Privacy Policy
Please subscribe me to the CodeProject newsletters

When answering a question please:

Read the question carefully.
Understand that English isn't everyone's first language so be lenient of bad spelling and grammar.
If a question is poorly phrased then either ask for clarification, ignore it, or edit the question and fix the problem. Insults are not welcome.
Don't tell someone to read the manual. Chances are they have and don't get it. Provide an answer or move on to the next question.

Let's work to help developers, not make them feel stupid.

This content, along with any associated source code and files, is licensed under The Code Project Open License (CPOL)

Richard MacCutchan · Answer 1 · 2018-12-03T01:37:00

Solution 2

How is it you could not find Concise Promela Reference[^]? Both (and all other statements) are clearly explained.

Posted 3-Dec-18 1:37am

Richard MacCutchan

Comments

Member 14075527 3-Dec-18 7:50am

Thank you. I was reading that but like I said it wasn't 100% clear to me as my mother tongue is not english. Do I understand it right if I say that the break statement can only break out of the loop or in this case the do-repitation and not the entire proctype? And the skip doesn't really do anything?

Richard MacCutchan 3-Dec-18 8:31am

Yes, that is correct.

[no name] 3-Dec-18 7:51am

+5. What a funny language: "Skip: Has no effect and is mainly used to satisfy syntactic requirements". So a "high level NOP" :-)

Member 14075527 3-Dec-18 7:52am

What do they mean by syntactic requirements?

[no name] 3-Dec-18 7:57am

Maybe this helps: Promela Reference -- skip(1)[^]

and this: An Overview of PROMELA | Types of Objects | InformIT[^]

Have a look to the while(a!=b) example in the second link. This should explain the use of skip. It Looks also that mostly you can rewrite the code to avoid skip

Member 14075527 3-Dec-18 8:24am

Thank you for the second link. I think I got know what skip does. The only thing that I still need to know is what exactly break does. Does it only break out of the do-repetition so that the code below the do-repetion will be executed/reached or does it block/wait the code below?

[no name] 3-Dec-18 8:36am

Keep in mind I'm not familar with PROMELA. But what written here Promela Reference -- break(3)[^] especally in "NOTES"

NOTES
It is an error to place a break statement where there is no surrounding repetition structure. The effect of a break statement can always be replicated with the use of a goto statement and a label.

I would guess it is a non blocking Statement.

Patrice T · Answer 2 · 2018-12-03T00:30:00

Solution 1

Quote:
What exactly is the difference between skip and break in PROMELA?

This is probably not the best place to ask.
Why don't you ask the makers ?
Why don't you read documentation ?
Why don't you ask in a users forum ?
Why don't you try to use debugger to see what ir going on ?

Posted 3-Dec-18 0:30am

Patrice T

Comments

Member 14075527 3-Dec-18 7:15am

I researched but it still isn't clear to me. The users forum doesn't accept new members.