implementations.py 19.1 KB
Newer Older
Michele's avatar
Michele committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
# Copyright (c) 2015 Michele Volpato
#
# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to deal
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
#
# The above copyright notice and this permission notice shall be included in
# all copies or substantial portions of the Software.
#
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
# THE SOFTWARE.

21
# Classes representing different kind of (Input Output) Labelled Transition
Michele's avatar
Michele committed
22
# Systems
23
from .baselts import AbstractIOLTS
Michele's avatar
Michele committed
24
import random
Michele's avatar
Michele committed
25
import graphviz as gv
26
import numpy as np
27 28
import helpers.bisimulation as bi
import logging
Michele's avatar
Michele committed
29 30

class InputOutputLTS(AbstractIOLTS):
31

Michele's avatar
Michele committed
32
    def __init__(self, numstates, inputs, outputs, quiescence = 'DELTA',
33 34 35 36
                 transitions = None, logger = None):

        self._logger = logger or logging.getLogger(__name__)

Michele's avatar
Michele committed
37
        # Every LTS has at least 1 state
Michele's avatar
Michele committed
38 39
        if numstates < 1:
            numstates = 1
40

41
        self._current = 0
42 43
        self._inputs = inputs.copy()
        self._outputs = outputs.copy()
Michele's avatar
Michele committed
44
        self._numstates = numstates
Michele's avatar
Michele committed
45
        self._quiescence = quiescence
46 47
        if not transitions:
            transitions={}
48
        self._transitions = transitions.copy()
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65

    # Return set of inputs
    def getInputs(self):
        return self._inputs

    # Return set of outputs
    def getOutputs(self):
        return self._outputs

    # Return number of states
    def getNumStates(self):
        return self._numstates

    # Return symbol for quiescence
    def getQuiescence(self):
        return self._quiescence

66
    # Return transitions
Michele's avatar
Michele committed
67 68 69
    def getTransitions(self):
        return self._transitions

Michele's avatar
Michele committed
70 71 72
    # Return to initial state
    def reset(self):
        self._current = 0
73

Michele's avatar
Michele committed
74
    # Given the label 'label' return all possible states reachable from
75 76
    # state with that label.
    # If there is no transition leaving state state with that label,
Michele's avatar
Michele committed
77
    # return NONE
78 79 80 81
    def nextStates(self, label, givenState = None):
        if givenState == None:
            givenState = self._current
        key = (givenState, label)
82 83
        if key in self._transitions.keys():
            return self._transitions[key]
84 85
        elif label == self._quiescence and self._quiescence in self.outputs(givenState):
            return set([givenState])
86 87
        else:
            return None
Michele's avatar
Michele committed
88 89 90 91

    # Return current state
    def currentState(self):
        return self._current
92

93 94 95 96 97 98 99 100 101 102 103 104
    # Force machine to state
    def forceState(state):
        newState = None
        if state < self._numstates:
            self._current = state
            newState = state
        return newState

    # Return all possible outputs from givenState
    def outputs(self, givenState = None):
        if givenState == None:
            givenState = self._current
Michele's avatar
Michele committed
105 106 107
        keys = self._transitions.keys()
        possibleOutputs = set()
        for state,label in keys:
108
            if state != givenState or label not in self._outputs:
Michele's avatar
Michele committed
109 110 111 112 113
                continue
            possibleOutputs.add(label)
        if len(possibleOutputs) == 0:
            possibleOutputs.add(self._quiescence)
        return possibleOutputs
114

115 116 117 118 119 120 121 122 123 124 125 126
    # Return all possible inputs from givenState
    def inputs(self, givenState = None):
        if givenState == None:
            givenState = self._current
        keys = self._transitions.keys()
        possibleInputs = set()
        for state,label in keys:
            if state != givenState or label not in self._inputs:
                continue
            possibleInputs.add(label)
        return possibleInputs

127
    # Add transition from state1 to state2 with label
Michele's avatar
Michele committed
128 129
    def addTransition(self, state1, label, state2):
        success = True
Michele's avatar
Michele committed
130 131 132
        validState1 = state1 < self._numstates and state1 >= 0
        validState2 = state2 < self._numstates and state2 >= 0
        if validState1 and validState2:
133
            #if label in self._inputs: #or label in self._outputs:
Michele's avatar
Michele committed
134 135 136 137 138
                key = (state1, label)
                if key in self._transitions.keys():
                    self._transitions[key].add(state2)
                else:
                    self._transitions[key] = set([state2])
139 140
            #else:
            #    success = False
Michele's avatar
Michele committed
141 142 143
        else:
            success = False
        return success
144 145

    # Move to a new state, from current with label
Michele's avatar
Michele committed
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161
    # Return (new) current state
    # If forceState is not in the set of reachabel states, return None
    # If label is not enabled return None
    def move(self, label, forceState=None):
        newState = self.currentState()
        if self.nextStates(label) != None:
            if forceState == None:
                newState = random.sample(self.nextStates(label), 1)[0]
            elif forceState not in self.nextStates(label):
                newState = None
            else:
                newState = forceState
        else:
            newState = None
        if newState != None:
            self._current = newState
Michele's avatar
Michele committed
162
        return newState
163 164 165 166 167 168 169 170 171 172

    # Check if the transition system is input enabled
    # i.e. for each state, for each input label, there is
    # a transition leaving that state with that label
    def isInputEnabled(self):
        isInputEnabled = True
        for state in range(0,self._numstates):
            for input in self._inputs:
                if (state, input) not in self._transitions.keys():
                    isInputEnabled = False
173
                    break
174 175 176 177 178 179 180 181 182 183
                else:
                    key = (state, input)
        return isInputEnabled

    # Add self loops to reach input enabledness
    def makeInputEnabled(self):
        for state in range(0,self._numstates):
            for input in self._inputs:
                if (state, input) not in self._transitions.keys():
                    self.addTransition(state, input, state)
184 185 186 187 188 189

# A suspension automaton is a particular LTS where quiescence is made
# explicit. The underling graph of a suspension automaton is deterministic,
# thus redefine addTransition
class SuspensionAutomaton(InputOutputLTS):

190 191 192 193
    def __init__(self, numStates, inputs, outputs, quiescence = 'DELTA',
                 chaos=False, logger=None):
        InputOutputLTS.__init__(self, numStates, inputs, outputs, quiescence,
                                logger=logger)
194 195 196 197 198 199 200 201 202 203 204 205 206
        # Quiescence is explicit: add it to outputs
        self._outputs.add(quiescence)

        # Chaotic behaviour:
        # Add two states: -1 and -2. The first one accepts every input and
        # output and also quiescence. The other is a support state given the
        # particular behaviour of quiescence. States are implicit, given
        # the quantity, thus it's enough to set a flag.
        self._isChaotic = chaos
        if chaos:
            # Add transitions between the two chaotic states
            self._addChaoticTransitions()

207 208 209
        # Discounted reachability (for calculating preciseness)
        self._discount = 0.5

210 211
    def isChaotic(self):
        return self._isChaotic
Michele's avatar
Michele committed
212 213 214 215 216 217 218

    def getChaos(self):
        return -1

    def getChaosDelta(self):
        return -2

219 220
    def _addChaoticTransitions(self):
        for input in self._inputs:
Michele's avatar
Michele committed
221 222
            self.addTransition(self.getChaos(), input, self.getChaos())
            self.addTransition(self.getChaosDelta(), input, self.getChaos())
223 224
        for output in self._outputs:
            if output != self._quiescence:
Michele's avatar
Michele committed
225 226 227 228 229
                self.addTransition(self.getChaos(), output, self.getChaos())
        self.addTransition(self.getChaos(), self._quiescence,
                           self.getChaosDelta())
        self.addTransition(self.getChaosDelta(), self._quiescence,
                           self.getChaosDelta())
230 231 232 233 234

    # Add transition from state1 to state2 with label
    # check if determinism is preserved
    def addTransition(self, state1, label, state2):
        # if there is already an entry in the transitions dictionary then
235
        # adding this transition would break determinism
236 237 238 239
        if (state1, label) in self._transitions.keys():
            return False
        # if we are adding a transition involving chaotic states (only
        # as state2), then add it directly.
Michele's avatar
Michele committed
240
        if state2 in set([self.getChaos(),self.getChaosDelta()]):
241 242
            if not self._isChaotic:
                return False
243 244 245 246
            if  state1 < self._numstates:
                if label in self._inputs or label in self._outputs:
                    key = (state1, label)
                    self._transitions[key] = set([state2])
247
                    return True
248 249 250
        else:
            # otherwise call superclass method
            return InputOutputLTS.addTransition(self, state1, label, state2)
251 252

    def preciseness(self):
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351
        if not self.isChaotic():
            return 1

        # breadth first search to find n reachability of set(-1,-2)
        # starting from chaotic states
        queue = [self.getChaos()]
        # visited states
        visited = []
        while queue:
            # dequeue
            current = queue.pop(0)
            visited.append(current)
            adjacents = [x for (x,label) in self._transitions.keys() \
                         if current in self._transitions[(x,label)]]
            for adjacent in adjacents:
                if not adjacent in visited + queue:
                    # enqueue
                    queue.append(adjacent)

        chaos = set([self.getChaos(), self.getChaosDelta()])
        # Get parents of a Chaotic states and the probability to reach
        # a chaotic state from them.
        probabilitiesOne = {}
        distanceOne = [x for (x,label) in self._transitions.keys() \
                if (self._transitions[(x,label)].intersection(chaos) != set() and
                x not in chaos)]
        for state in distanceOne:
            # total transitions from state
            totTrans = len([l for (s, l) in self._transitions.keys() \
                        if s == state])
            # num transitions from state to chaos
            numTrans = len([l for (s, l) in self._transitions.keys() \
                        if (self._transitions[(s,l)].intersection(chaos) != set() and
                            s == state)])
            probabilitiesOne[state] = (numTrans,totTrans)

        # visited now contains all states that can reach Chaos
        # probabilitiesOne contains all state with distance one and the
        # probabilities to get to Chaos from them

        # for each state, get the linear equation describing the rechability
        # of chaos
        equations = []
        values = []
        for state in range(self.getNumStates()):
            # if Chaos is not reacheble, then state-th variable is 0
            if state not in visited:
                equation = []
                for stateVar in range(self.getNumStates()):
                    if stateVar != state:
                        equation.append(0)
                    else:
                        equation.append(1)
                equations.append(equation)
                values.append(0)
                continue

            # if we are in a chaotic state then variable is 1
            if state in [self.getChaos(),self.getChaosDelta()]:
                equation = []
                for stateVar in range(self.getNumStates()):
                    if stateVar != state:
                        equation.append(0)
                    else:
                        equation.append(1)
                equations.append(equation)
                values.append(1)
                continue

            # otherwise construct linear equation
            equation = []
            # total transitions from state
            totTrans = len([l for (s, l) in self._transitions.keys() \
                        if s == state])
            for stateVar in range(self.getNumStates()):
                # Important! stateVar cannot be in Chaos

                # num transitions from state to statVar
                numTrans = len([l for (s, l) in self._transitions.keys() \
                    if (stateVar in self._transitions[(s,l)] and
                    s == state)])
                if stateVar != state:
                    equation.append(self._discount * numTrans / totTrans)
                else:
                    # format: stateVar = a*x1 + b*x2 + ... + c * stateVar + d
                    equation.append((self._discount * numTrans / totTrans)-1)
            equations.append(equation)
            # Reachability with one step
            if state in probabilitiesOne.keys():
                (numTrans,totTrans) = probabilitiesOne[state]
                values.append(-(numTrans / totTrans))
            else:
                values.append(0)

        a = np.array(equations)
        b = np.array(values)
        x = np.linalg.solve(a, b)
        # 1 - discounted reachability of chaos from first state
        return 1 - x[0]
352 353 354 355 356 357 358 359

    # Check if the suspension automaton is valid.
    # Willemse T.A.C.: Heuristics for ioco-based test-based modelling
    def isValid(self):
        return (self.isNonBlocking() and self.isQuiescenceReducible() and
                self.isAnomalyFree() and self.isStable())

    def isNonBlocking(self):
360 361 362 363 364 365 366 367 368 369 370 371 372 373 374
        # ∀q ∈ Q, ∃λ ∈ L_U ∪ {δ} . q λ→ (for each state there is an
        # output transition leaving that state, or quiescence)
        for state in range(self._numstates):
            found = False
            for label in self._outputs: # quiescence is in self._outputs
                if (state, label) in self._transitions.keys():
                    # found a transition
                    found = True
                    exit
            if found == False:
                # if we did not find an output transition return false
                # otherwise go to next state
                return False
        # If we never returned False, then we passed all states and found
        # an output transition for each of them
375 376 377
        return True

    def isQuiescenceReducible(self):
378 379
        # ∀q ∈ Q, ∀σ ∈ L^∗_δ . δ·σ ∈ traces(q) => σ ∈ traces(q)
        # checked by simulation algorithm
380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431
        # function used for filtering states that enable some label
        stateWithLabel = lambda label: lambda x: (x,label) \
                                in self._transitions.keys()
        # past contains the pair of states already visited.
        # If I visited already a pair for one loop of the following for loop,
        # I do not need to check it again for other loops. Thus past is outside
        # the for loop.
        past = set()
        # filter states
        for state1 in filter(stateWithLabel(self.getQuiescence()),
                              range(self.getNumStates())):

            # Suspension automata are "deterministic"
            state2 = next(iter(self._transitions[(state1, self.getQuiescence())]))

            if state1 == state2:
                # same state, simulation is trivial
                continue

            if (state1, state2) in past:
                # I already visited this pair. Go to next state enabling quiescence
                continue

            wait = set()
            wait.add((state1, state2))
            while wait:
                current = wait.pop()
                past.add((current[0],current[1]))
                # TODO: input enabledness?

                labels = self._inputs.union(self._outputs)
                for label in labels:
                    if (state2, label) not in self._transitions.keys():
                        # This label is not enabled in state 2, no need to check
                        continue
                    elif (state1, label) not in self._transitions.keys():
                        # Found a counterexample!
                        return False
                    else:
                        # Both enable label, follow label and add next pair of
                        # states in wait queue
                        newState1 =  next(iter(self._transitions[(state1, label)]))
                        newState2 =  next(iter(self._transitions[(state2, label)]))

                        if ((newState1,newState2) not in past
                            and newState1 != newState2):
                            wait.add((newState1, newState2))

        # No counterexample to quiescence reducibility has been found.
        return True

    def isAnomalyFree(self):
432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
        # ∀q ∈ Q, ∀λ ∈ L_U . δ·λ not ∈ traces(q)
        # each state reached by quiescence does not enable any other output

        # list of quiescence transitions
        qTransitions = [x for x in self._transitions.keys() \
                        if x[1] == self._quiescence]

        # list of states that I already checked
        checked = []
        for (start, quiescence) in qTransitions:
            for state in self._transitions[(start, quiescence)]:
                if state not in checked:
                    checked.append(state)
                    if len(self.outputs(state)) > 1:
                        # More than one output enabled, quiescence + something
                        return False
                    elif self._quiescence not in self.outputs(state):
                        # only one output enabled, but not quiescence
                        return False

452 453 454
        return True

    def isStable(self):
455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485
        # TODO: this method could be improved with a custom bisimulation
        # we can avoid checking the same couple of state multiple
        # times.

        # ∀q, q' , q'' ∈ Q . q δ→ q' δ→ q'' => traces(q' ) = traces(q'' )
        # After two delta transitions, there must be a bisimulation relation
        # between the last two states.

        # list of quiescence transitions
        qTransitions = [x for x in self._transitions.keys() \
                        if x[1] == self._quiescence]

        # list of pair of states that I already checked
        checked = []
        for (start, quiescence) in qTransitions:
            for state1 in self._transitions[(start, quiescence)]:
                states2 = self.nextStates(quiescence, state1)
                if len(states2) != 1:
                    # something is wrong, either non deterministic, or
                    # quiescence is not enabled.
                    self._logger.warning("Suspension automaton either " +
                            "nondeterministic or does not enable quiescence" +
                            " where it should.")
                    return False
                for state2 in states2:
                    # get the only element of states2
                    break
                if (state1, state2) not in checked and state1 != state2:
                    checked.append((state1, state2))
                    if not bi.bisimilar(self, self, state1, state2):
                        return False
486
        return True