FilesExpand file tree

 develop

/

pycanlib.pml

Copy path

Blame

More file actions

Blame

More file actions

Latest commit

 

History

History

History

91 lines (79 loc) · 1.3 KB

 develop

/

pycanlib.pml

Copy path

Top

File metadata and controls

• Code
• Blame

91 lines (79 loc) · 1.3 KB

Raw

Copy raw file

Download raw file

Open symbols panel

Edit and raw actions

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

65

66

67

68

69

70

71

72

73

74

75

76

77

78

79

80

81

82

83

84

85

86

87

88

89

90

91

/* This promela model was used to verify the concurrent design of the bus object. */

bool lock = false;

inline enterMon() {

atomic {

!lock;

lock = true;

}

}

inline leaveMon() {

lock = false;

}

typedef Condition {

bool gate;

byte waiting;

}

#define emptyC(C) (C.waiting == 0)

inline waitC(C) {

atomic {

C.waiting++;

lock = false;

C.gate;

C.gate = false;

C.waiting--;

}

}

inline signalC(C) {

atomic {

if

:: (C.waiting > 0) ->

C.gate = true;

!lock;

lock = true;

:: else

fi;

}

}

mtype = { clear, set };

mtype writing_event = clear;

byte critical = 0;

Condition done_writing;

bool live = false;

active proctype RX()

{

end:

do

:: enterMon();

if

:: (writing_event == set) ->

waitC(done_writing);

:: else

fi;

critical++;

assert(critical == 1);

live = true;

live = false;

critical--;

leaveMon();

od

}

active proctype TX()

{

end:

do

:: atomic {

writing_event == clear ->

writing_event = set;

}

enterMon();

critical++;

assert(critical == 1);

live = true;

live = false;

critical--;

writing_event = clear;

signalC(done_writing);

leaveMon();

od

}

ltl {[]<> live}