--%>

State-space Reduction in Promela model

State-space Reduction: Two language statements are used to reduce the number of states in a Promela model: atomic and d-step.

1553_state space.jpg

Atomic is used to group statements of a particular process into one atomic sequence. The statements are executed in a single step and are not interleaved with statements of other processes. The atomicity is broken if any of the statements is blocking. That is, statements of other processes can be interleaved in between.

d-step can also be used to execute a number of statements in one step. The difference is that no intermediate states are generated or stored. If one of the statements blocks, this is considered a runtime error.

   Related Questions in Programming Languages

  • Q : Explain the way to start a Web Service

    Explain the way to start a Web Service.

  • Q : What is Server Server : Something which

    Server: Something which gives a service. The Web server delivers resources to its clients, for example. Whenever the server is an object, this is the recipient of messages from its object clients.

  • Q : Directory and filename Explain

    Explain directory and filename?

  • Q : Define Anonymous object Anonymous

    Anonymous object: An object formed without an identifier. They are generally formed as array elements, actual arguments or method outcomes. For example:     private Point[] vertices = { &n

  • Q : Define Continue statement Continue

    Continue statement: A statement which might only be employed within the body of a loop. In case of a while loop or do loop, control passes instantly to the loop's terminating test. In case of a for loop, the control passes to the post-body update expr

  • Q : Search and Partial Coverage of Java

    Search and Partial Coverage: JPF supports well-known search strategies such as BFS and DFS as well as various heuristic-based searches such as A*, Best-First, and Beam Search. You can sum a number of heuristics during the search, and set search depth

  • Q : What is sticky bit Explain the sticky

    Explain the sticky bit?

  • Q : Reducing state space of code What is

    What is the way to reduce the state space of the code during model checking?

  • Q : What is Class Selector in the CSS

    Explain what is meant by the Class Selector in the CSS?

  • Q : Explain Wrapper classes Wrapper

    Wrapper classes: The Java's primitive types are not of object types. The wrapper classes are stated in the java.lang package. They comprises of a class for each and every primitive type: Boolean, Byte, Double, Float, Integer, Long & Short and Char