Promela
ಪ್ರೋಮೆಲಾ (ಪ್ರೊಸೆಸ್ ಅಥವಾ ಪ್ರೊಟೊಕಾಲ್ ಮೆಟಾ ಲ್ಯಾಂಗ್ವೇಜ್) ಎಂಬುದು ಗೆರಾರ್ಡ್ ಜೆ. ಹೋಲ್ಜ್ಮನ್ ಪರಿಚಯಿಸಿದ ಪರಿಶೀಲನಾ ಮಾದರಿ ಭಾಷೆಯಾಗಿದೆ. ಈ ಭಾಷೆಯು ಮಾದರಿಗಳಿಗೆ, ಉದಾಹರಣೆಗೆ, ವಿತರಣಾ ವ್ಯವಸ್ಥೆಗಳಿಗೆ, ಏಕಕಾಲೀನ ಪ್ರಕ್ರಿಯೆಗಳ ಕ್ರಿಯಾತ್ಮಕ ಸೃಷ್ಟಿಗೆ ಅನುವು ಮಾಡಿಕೊಡುತ್ತದೆ. PROMELA ಮಾದರಿಗಳಲ್ಲಿ, ಸಂದೇಶ ಚಾನೆಲ್ಗಳ ಮೂಲಕ ಸಂವಹನವನ್ನು ಸಿಂಕ್ರೊನಸ್ (ಅಂದರೆ, ಸಂಧಿಸ್ಥಾನ), ಅಥವಾ ಅಸಿಂಕ್ರೊನಸ್ (ಅಂದರೆ, ಬಫರ್ಡ್) ಎಂದು ವ್ಯಾಖ್ಯಾನಿಸಬಹುದು. ಮಾದರಿಯ ವ್ಯವಸ್ಥೆಯು ಅಪೇಕ್ಷಿತ ನಡವಳಿಕೆಯನ್ನು ಉತ್ಪಾದಿಸುತ್ತದೆ ಎಂಬುದನ್ನು ಪರಿಶೀಲಿಸಲು ಪ್ರೋಮೆಲಾ ಮಾದರಿಗಳನ್ನು ಸ್ಪಿನ್ ಮಾದರಿ ಪರೀಕ್ಷಕದೊಂದಿಗೆ ವಿಶ್ಲೇಷಿಸಬಹುದು. ಕಂಪ್ಯೂಟರ್ ಏಡೆಡ್ ವೆರಿಫಿಕೇಷನ್ ಆಫ್ ಆಟೋಮ್ಯಾಟಾ (ಸಿಎವಿಎ) ಯೋಜನೆಯ ಭಾಗವಾಗಿ ಇಸಾಬೆಲ್ಲೆ/ಎಚ್ಓಎಲ್ನೊಂದಿಗೆ ಪರಿಶೀಲಿಸಿದ ಅನುಷ್ಠಾನವೂ ಲಭ್ಯವಿದೆ. ಪ್ರೋಮೆಲಾದಲ್ಲಿ ಬರೆಯಲಾದ ಕಡತಗಳು ಸಾಂಪ್ರದಾಯಿಕವಾಗಿ. ಪಿ. ಎಂ. ಎಲ್ ಕಡತ ವಿಸ್ತರಣೆಯನ್ನು ಹೊಂದಿರುತ್ತವೆ. ಪರಿಚಯ PROMELA ಒಂದು ಪ್ರಕ್ರಿಯೆ-ಮಾದರಿ ಭಾಷೆಯಾಗಿದ್ದು, ಸಮಾನಾಂತರ ವ್ಯವಸ್ಥೆಗಳ ತರ್ಕವನ್ನು ಪರಿಶೀಲಿಸುವುದು ಇದರ ಉದ್ದೇಶವಾಗಿದೆ. ಪ್ರೋಮೆಲಾದಲ್ಲಿ ಒಂದು ಪ್ರೋಗ್ರಾಂ ಅನ್ನು ನೀಡಿದರೆ, ಮಾದರಿಯ ವ್ಯವಸ್ಥೆಯ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯ ಯಾದೃಚ್ಛಿಕ ಅಥವಾ ಪುನರಾವರ್ತಿತ ಸಿಮ್ಯುಲೇಶನ್ಗಳನ್ನು ನಿರ್ವಹಿಸುವ ಮೂಲಕ ಸ್ಪಿನ್ ಮಾದರಿಯನ್ನು ನಿಖರತೆಗಾಗಿ ಪರಿಶೀಲಿಸಬಹುದು, ಅಥವಾ ಇದು ಸಿಸ್ಟಮ್ ಸ್ಟೇಟ್ ಸ್ಪೇಸ್ನ ತ್ವರಿತ ಸಮಗ್ರ ಪರಿಶೀಲನೆಯನ್ನು ನಿರ್ವಹಿಸುವ ಸಿ ಪ್ರೋಗ್ರಾಂ ಅನ್ನು ರಚಿಸಬಹುದು. ಸಿಮ್ಯುಲೇಶನ್ಗಳು ಮತ್ತು ಪರಿಶೀಲನೆಗಳ ಸಮಯದಲ್ಲಿ, ಡೆಡ್ಲಾಕ್ಗಳು, ಅನಿರ್ದಿಷ್ಟ ಸ್ವಾಗತಗಳು ಮತ್ತು ಕಾರ್ಯಗತಗೊಳಿಸಲಾಗದ ಕೋಡ್ಗಳ ಅನುಪಸ್ಥಿತಿಯನ್ನು ಸ್ಪಿನ್ ಪರಿಶೀಲಿಸುತ್ತದೆ. ವ್ಯವಸ್ಥೆಯ ಅಸ್ಥಿರಗಳ ನಿಖರತೆಯನ್ನು ಸಾಬೀತುಪಡಿಸಲು ಸಹ ಪರಿಶೀಲನಾ ಯಂತ್ರವನ್ನು ಬಳಸಬಹುದು ಮತ್ತು ಇದು ಪ್ರಗತಿಯಲ್ಲದ ಕಾರ್ಯಗತಗೊಳಿಸುವ ಚಕ್ರಗಳನ್ನು ಕಂಡುಹಿಡಿಯಬಹುದು. ಅಂತಿಮವಾಗಿ, ಇದು ರೇಖೀಯ ಸಮಯದ ತಾತ್ಕಾಲಿಕ ನಿರ್ಬಂಧಗಳ ಪರಿಶೀಲನೆಯನ್ನು ಬೆಂಬಲಿಸುತ್ತದೆ; ಪ್ರೋಮೆಲಾ ಎಂದಿಗೂ ಹೇಳಿಕೊಳ್ಳುವುದಿಲ್ಲ ಅಥವಾ ತಾತ್ಕಾಲಿಕ ತರ್ಕದಲ್ಲಿ ನಿರ್ಬಂಧಗಳನ್ನು ನೇರವಾಗಿ ರೂಪಿಸುವ ಮೂಲಕ. ಪ್ರತಿಯೊಂದು ಮಾದರಿಯನ್ನು ಪರಿಸರದ ಬಗೆಗಿನ ವಿವಿಧ ರೀತಿಯ ಊಹೆಗಳ ಅಡಿಯಲ್ಲಿ ಸ್ಪಿನ್ ಮೂಲಕ ಪರಿಶೀಲಿಸಬಹುದು. ಒಂದು ಮಾದರಿಯ ನಿಖರತೆಯನ್ನು ಸ್ಪಿನ್ ಮೂಲಕ ಸ್ಥಾಪಿಸಿದ ನಂತರ, ಆ ಸಂಗತಿಯನ್ನು ನಂತರದ ಎಲ್ಲಾ ಮಾದರಿಗಳ ನಿರ್ಮಾಣ ಮತ್ತು ಪರಿಶೀಲನೆಯಲ್ಲಿ ಬಳಸಬಹುದು. PROMELA ಪ್ರೋಗ್ರಾಂಗಳು ಪ್ರಕ್ರಿಯೆಗಳು, ಸಂದೇಶ ಚಾನೆಲ್ಗಳು ಮತ್ತು ಅಸ್ಥಿರಗಳನ್ನು ಒಳಗೊಂಡಿರುತ್ತವೆ. ಪ್ರಕ್ರಿಯೆಗಳು ವಿತರಣಾ ವ್ಯವಸ್ಥೆಯ ಏಕಕಾಲೀನ ಘಟಕಗಳನ್ನು ಪ್ರತಿನಿಧಿಸುವ ಜಾಗತಿಕ ವಸ್ತುಗಳು. ಸಂದೇಶ ಚಾನೆಲ್ಗಳು ಮತ್ತು ಅಸ್ಥಿರಗಳನ್ನು ಒಂದು ಪ್ರಕ್ರಿಯೆಯೊಳಗೆ ಜಾಗತಿಕವಾಗಿ ಅಥವಾ ಸ್ಥಳೀಯವಾಗಿ ಘೋಷಿಸಬಹುದು. ಪ್ರಕ್ರಿಯೆಗಳು ನಡವಳಿಕೆಯನ್ನು ನಿರ್ದಿಷ್ಟಪಡಿಸುತ್ತವೆ, ಮಾರ್ಗಗಳು ಮತ್ತು ಜಾಗತಿಕ ಅಸ್ಥಿರಗಳು ಪ್ರಕ್ರಿಯೆಗಳು ನಡೆಯುವ ಪರಿಸರವನ್ನು ವ್ಯಾಖ್ಯಾನಿಸುತ್ತವೆ. ಭಾಷಾ ಉಲ್ಲೇಖ ದತ್ತಾಂಶ ಪ್ರಕಾರಗಳು ಪ್ರೋಮೆಲಾದಲ್ಲಿ ಬಳಸಲಾಗುವ ಮೂಲ ದತ್ತಾಂಶ ಪ್ರಕಾರಗಳನ್ನು ಕೆಳಗಿನ ಕೋಷ್ಟಕದಲ್ಲಿ ಪ್ರಸ್ತುತಪಡಿಸಲಾಗಿದೆ. ಪಿಸಿ ಐ386/ಲಿನಕ್ಸ್ ಯಂತ್ರಕ್ಕಾಗಿ ಬಿಟ್ಗಳಲ್ಲಿನ ಗಾತ್ರಗಳನ್ನು ನೀಡಲಾಗಿದೆ. ಬಿಟ್ ಮತ್ತು ಬೂಲ್ ಎಂಬ ಹೆಸರುಗಳು ಒಂದೇ ಮಾಹಿತಿಯ ಸಮಾನಾರ್ಥಕಗಳಾಗಿವೆ. ಬೈಟ್ ಒಂದು ಸಹಿ ಮಾಡದ ಪ್ರಮಾಣವಾಗಿದ್ದು ಅದು 0 ಮತ್ತು 255ರ ನಡುವಿನ ಮೌಲ್ಯವನ್ನು ಸಂಗ್ರಹಿಸಬಲ್ಲದು. ಶಾರ್ಟ್ಸ್ ಮತ್ತು ಇಂಟ್ಗಳು ಸಹಿ ಮಾಡಲಾದ ಪ್ರಮಾಣಗಳಾಗಿದ್ದು ಅವು ಹಿಡಿದಿಟ್ಟುಕೊಳ್ಳಬಹುದಾದ ಮೌಲ್ಯಗಳ ವ್ಯಾಪ್ತಿಯಲ್ಲಿ ಮಾತ್ರ ಭಿನ್ನವಾಗಿರುತ್ತವೆ. ವೇರಿಯೇಬಲ್ಗಳನ್ನು ಸಹ ವ್ಯೂಹಗಳೆಂದು ಘೋಷಿಸಬಹುದು. ಉದಾಹರಣೆಗೆ, ಘೋಷಣೆಯುಃ ಶ್ರೇಣಿಯನ್ನು ಚಂದಾದಾರಿಕೆ ಅಭಿವ್ಯಕ್ತಿಗಳಲ್ಲಿ ಪ್ರವೇಶಿಸಬಹುದಾದ 10 ಪೂರ್ಣಾಂಕಗಳ ಶ್ರೇಣಿಯನ್ನು ಘೋಷಿಸುತ್ತದೆಃ x [0] = x [1] + x [2]; ಆದರೆ ರಚನೆಯ ಮೇಲೆ ಸರಣಿಗಳನ್ನು ಎಣಿಸಲಾಗುವುದಿಲ್ಲ, ಆದ್ದರಿಂದ ಅವುಗಳನ್ನು ಈ ಕೆಳಗಿನಂತೆ ಪ್ರಾರಂಭಿಸಬೇಕುಃ ರಚನೆಯ ಸೂಚ್ಯಂಕವು ಒಂದು ಅನನ್ಯ ಪೂರ್ಣಾಂಕ ಮೌಲ್ಯವನ್ನು ನಿರ್ಧರಿಸುವ ಯಾವುದೇ ಅಭಿವ್ಯಕ್ತಿಯಾಗಿರಬಹುದು. ಶ್ರೇಣಿಯ ಹೊರಗಿನ ಸೂಚ್ಯಂಕದ ಪರಿಣಾಮವನ್ನು ವ್ಯಾಖ್ಯಾನಿಸಲಾಗಿಲ್ಲ. ಬಹು-ಆಯಾಮದ ವ್ಯೂಹಗಳನ್ನು ಟೈಪೆಡೆಫ್ ರಚನೆಯ ಸಹಾಯದಿಂದ ಪರೋಕ್ಷವಾಗಿ ವ್ಯಾಖ್ಯಾನಿಸಬಹುದು (ಕೆಳಗೆ ನೋಡಿ). ಪ್ರಕ್ರಿಯೆಗಳು ವೇರಿಯೇಬಲ್ ಅಥವಾ ಸಂದೇಶ ಚಾನೆಲ್ನ ಸ್ಥಿತಿಯನ್ನು ಪ್ರಕ್ರಿಯೆಗಳಿಂದ ಮಾತ್ರ ಬದಲಾಯಿಸಬಹುದು ಅಥವಾ ಪರಿಶೀಲಿಸಬಹುದು. ಒಂದು ಪ್ರಕ್ರಿಯೆಯ ನಡವಳಿಕೆಯನ್ನು ಪ್ರಾಕ್ಟೈಪ್ ಘೋಷಣೆಯಿಂದ ವ್ಯಾಖ್ಯಾನಿಸಲಾಗಿದೆ. ಉದಾಹರಣೆಗೆ, ಈ ಕೆಳಗಿನವುಗಳು ಒಂದು ವೇರಿಯೇಬಲ್ ಸ್ಥಿತಿಯೊಂದಿಗೆ ಎ ಪ್ರಕ್ರಿಯೆಯ ಪ್ರಕಾರವನ್ನು ಘೋಷಿಸುತ್ತವೆಃ ಪ್ರಾಕ್ಟೈಪ್ ಎ () {ಬೈಟ್ ಸ್ಥಿತಿ; ಸ್ಥಿತಿ = 3;} ಪ್ರಾಕ್ಟೈಪ್ ವ್ಯಾಖ್ಯಾನವು ಪ್ರಕ್ರಿಯೆಯ ನಡವಳಿಕೆಯನ್ನು ಮಾತ್ರ ಘೋಷಿಸುತ್ತದೆ, ಅದು ಅದನ್ನು ಕಾರ್ಯಗತಗೊಳಿಸುವುದಿಲ್ಲ. ಆರಂಭದಲ್ಲಿ, PROMELA ಮಾದರಿಯಲ್ಲಿ, ಕೇವಲ ಒಂದು ಪ್ರಕ್ರಿಯೆಯನ್ನು ಕಾರ್ಯಗತಗೊಳಿಸಲಾಗುತ್ತದೆಃ ಪ್ರತಿ PROMELA ವಿವರಣೆಯಲ್ಲಿ ಸ್ಪಷ್ಟವಾಗಿ ಘೋಷಿಸಬೇಕಾದ init ಪ್ರಕಾರದ ಪ್ರಕ್ರಿಯೆ. ರನ್ ಸ್ಟೇಟ್ಮೆಂಟ್ ಅನ್ನು ಬಳಸಿಕೊಂಡು ಹೊಸ ಪ್ರಕ್ರಿಯೆಗಳನ್ನು ಹುಟ್ಟುಹಾಕಬಹುದು, ಇದು ಪ್ರಾಕ್ಟೈಪ್ನ ಹೆಸರನ್ನು ಒಳಗೊಂಡಿರುವ ವಾದವನ್ನು ತೆಗೆದುಕೊಳ್ಳುತ್ತದೆ, ಇದರಿಂದ ಪ್ರಕ್ರಿಯೆಯನ್ನು ತ್ವರಿತಗೊಳಿಸಲಾಗುತ್ತದೆ. ರನ್ ಆಪರೇಟರ್ ಅನ್ನು ಪ್ರಾಕ್ಟೈಪ್ ವ್ಯಾಖ್ಯಾನಗಳ ಮುಖ್ಯಭಾಗದಲ್ಲಿ ಬಳಸಬಹುದು, ಆರಂಭಿಕ ಪ್ರಕ್ರಿಯೆಯಲ್ಲಿ ಮಾತ್ರವಲ್ಲ. ಇದು ಪ್ರೋಮೆಲಾದಲ್ಲಿ ಪ್ರಕ್ರಿಯೆಗಳ ಕ್ರಿಯಾತ್ಮಕ ಸೃಷ್ಟಿಗೆ ಅನುವು ಮಾಡಿಕೊಡುತ್ತದೆ. ಕಾರ್ಯಗತಗೊಳಿಸುವ ಪ್ರಕ್ರಿಯೆಯು ಕೊನೆಗೊಂಡಾಗ ಕಣ್ಮರೆಯಾಗುತ್ತದೆ-ಅಂದರೆ, ಅದು ಪ್ರಾಕ್ಟೈಪ್ ವ್ಯಾಖ್ಯಾನದಲ್ಲಿ ದೇಹದ ಅಂತ್ಯವನ್ನು ತಲುಪಿದಾಗ, ಮತ್ತು ಅದು ಪ್ರಾರಂಭಿಸಿದ ಎಲ್ಲಾ ಚೈಲ್ಡ್ ಪ್ರಕ್ರಿಯೆಗಳು ಕೊನೆಗೊಂಡಿವೆ. ಒಂದು ಪ್ರಾಕ್ಟೈಪ್ ಸಹ ಸಕ್ರಿಯವಾಗಿರಬಹುದು (ಕೆಳಗೆ). ಪರಮಾಣು ರಚನೆ ಪರಮಾಣು ಎಂಬ ಮುಖ್ಯ ಪದದೊಂದಿಗೆ ಸುರುಳಿಯಾಕಾರದ ಕಟ್ಟುಪಟ್ಟಿಗಳಲ್ಲಿ ಸುತ್ತುವರಿದ ಹೇಳಿಕೆಗಳ ಅನುಕ್ರಮವನ್ನು ಪೂರ್ವಪ್ರತ್ಯಯ ಮಾಡುವ ಮೂಲಕ, ಅನುಕ್ರಮವನ್ನು ಒಂದು ಅವಿಭಾಜ್ಯ ಘಟಕವಾಗಿ ಕಾರ್ಯಗತಗೊಳಿಸಬೇಕೆಂದು ಬಳಕೆದಾರರು ಸೂಚಿಸಬಹುದು, ಇದು ಇತರ ಯಾವುದೇ ಪ್ರಕ್ರಿಯೆಗಳೊಂದಿಗೆ ಬೆಸೆದುಕೊಂಡಿಲ್ಲ. ಪರಮಾಣು ಅನುಕ್ರಮಗಳು ಪರಿಶೀಲನಾ ಮಾದರಿಗಳ ಸಂಕೀರ್ಣತೆಯನ್ನು ಕಡಿಮೆ ಮಾಡುವಲ್ಲಿ ಪ್ರಮುಖ ಸಾಧನವಾಗಬಹುದು. ಪರಮಾಣು ಅನುಕ್ರಮಗಳು ವಿತರಣಾ ವ್ಯವಸ್ಥೆಯಲ್ಲಿ ಅನುಮತಿಸಲಾದ ಇಂಟರ್ಲೀವಿಂಗ್ನ ಪ್ರಮಾಣವನ್ನು ನಿರ್ಬಂಧಿಸುತ್ತವೆ ಎಂಬುದನ್ನು ಗಮನಿಸಿ. ಸ್ಥಳೀಯ ಅಸ್ಥಿರಗಳ ಎಲ್ಲಾ ಕುಶಲತೆಗಳನ್ನು ಪರಮಾಣು ಅನುಕ್ರಮಗಳೊಂದಿಗೆ ಲೇಬಲ್ ಮಾಡುವ ಮೂಲಕ ಜಟಿಲ ಮಾದರಿಗಳನ್ನು ಟ್ರ್ಯಾಕ್ ಮಾಡಬಹುದಾದಂತೆ ಮಾಡಬಹುದು. ಒಂದು ಪ್ರಕ್ರಿಯೆಯಿಂದ ಮತ್ತೊಂದು ಪ್ರಕ್ರಿಯೆಗೆ ದತ್ತಾಂಶದ ವರ್ಗಾವಣೆಯನ್ನು ರೂಪಿಸಲು ಸಂದೇಶ ರವಾನೆ ಸಂದೇಶ ವಾಹಿನಿಗಳನ್ನು ಬಳಸಲಾಗುತ್ತದೆ. ಅವುಗಳನ್ನು ಸ್ಥಳೀಯವಾಗಿ ಅಥವಾ ಜಾಗತಿಕವಾಗಿ ಈ ಕೆಳಗಿನಂತೆ ಘೋಷಿಸಲಾಗಿದೆಃ {ಷಾರ್ಟ್} ನ chan qname = [16] ಇದು ಬಫರ್ಡ್ ಚಾನೆಲ್ ಎಂದು ಘೋಷಿಸುತ್ತದೆ, ಇದು 16 ಸಂದೇಶಗಳ ಪ್ರಕಾರದ ಸಣ್ಣ ಸಂದೇಶಗಳನ್ನು ಸಂಗ್ರಹಿಸಬಹುದು (ಸಾಮರ್ಥ್ಯವು ಇಲ್ಲಿ 16 ಆಗಿದೆ). ಆ ಹೇಳಿಕೆಯುಃ "ಹೆಸರು!" ಎಕ್ಸ್ಪಿಆರ್; ಎಕ್ಸ್ಪಿಆರ್ ಅಭಿವ್ಯಕ್ತಿಯ ಮೌಲ್ಯವನ್ನು ಕ್ಯೂನೇಮ್ ಹೆಸರಿನೊಂದಿಗೆ ಚಾನೆಲ್ಗೆ ಕಳುಹಿಸುತ್ತದೆ, ಅಂದರೆ, ಇದು ಚಾನೆಲ್ನ ಬಾಲಕ್ಕೆ ಮೌಲ್ಯವನ್ನು ಸೇರಿಸುತ್ತದೆ. ಹೇಳಿಕೆಃ ಯಾವ ಹೆಸರು? ಎಂ. ಎಸ್. ಜಿ. ಸಂದೇಶವನ್ನು ಸ್ವೀಕರಿಸುತ್ತದೆ, ಅದನ್ನು ಚಾನೆಲ್ನ ತಲೆಯಿಂದ ಹಿಂಪಡೆಯುತ್ತದೆ ಮತ್ತು ಅದನ್ನು ಎಂ. ಎಸ್. ಜಿ. ವೇರಿಯೇಬಲ್ನಲ್ಲಿ ಸಂಗ್ರಹಿಸುತ್ತದೆ. ವಾಹಿನಿಗಳು ಸಂದೇಶಗಳನ್ನು ಫಸ್ಟ್-ಇನ್-ಫಸ್ಟ್-ಔಟ್ ಕ್ರಮದಲ್ಲಿ ರವಾನಿಸುತ್ತವೆ. ಒಂದು ಸಂಧಿಸ್ಥಾನದ ಬಂದರನ್ನು ಮಳಿಗೆಯ ಉದ್ದ ಶೂನ್ಯವಾಗಿರುವ ಸಂದೇಶದ ಮಾರ್ಗವೆಂದು ಘೋಷಿಸಬಹುದು. ಉದಾಹರಣೆಗೆ, ಈ ಕೆಳಗಿನವುಃ {ಬೈಟ್} ನ ಚಾನ್ ಪೋರ್ಟ್ = [0] ಬೈಟ್ ಪ್ರಕಾರದ ಸಂದೇಶಗಳನ್ನು ರವಾನಿಸಬಲ್ಲ ಸಂಧಿಸ್ಥಾನ ಪೋರ್ಟ್ ಅನ್ನು ವ್ಯಾಖ್ಯಾನಿಸುತ್ತದೆ. ಅಂತಹ ಸಂಧಿಸ್ಥಾನ ಬಂದರುಗಳ ಮೂಲಕ ಸಂದೇಶ ಸಂವಹನಗಳು ವ್ಯಾಖ್ಯಾನದ ಪ್ರಕಾರ ಸಿಂಕ್ರೊನಸ್ ಆಗಿರುತ್ತವೆ, ಅಂದರೆ. ಕಳುಹಿಸುವವರು ಅಥವಾ ಸ್ವೀಕರಿಸುವವರು (ಚಾನಲ್ಗೆ ಮೊದಲು ಬರುವವರು) ಎರಡನೇ ಬಾರಿಗೆ ಬರುವ ಸ್ಪರ್ಧಿಗೆ (ಸ್ವೀಕರಿಸುವವರು ಅಥವಾ ಕಳುಹಿಸುವವರು) ನಿರ್ಬಂಧಿಸುತ್ತಾರೆ. ಬಫರ್ಡ್ ಚಾನೆಲ್ ಅನ್ನು ಅದರ ಸಾಮರ್ಥ್ಯಕ್ಕೆ ತುಂಬಿಸಿದಾಗ (ಇನ್ಪುಟ್ಗಳನ್ನು ಸ್ವೀಕರಿಸುವ ಮೊದಲು "ಸಾಮರ್ಥ್ಯ" ಸಂಖ್ಯೆಯ ಔಟ್ಪುಟ್ಗಳನ್ನು ಕಳುಹಿಸುವುದು), ಚಾನೆಲ್ನ ಡೀಫಾಲ್ಟ್ ನಡವಳಿಕೆಯು ಸಿಂಕ್ರೊನಸ್ ಆಗಿರುತ್ತದೆ, ಮತ್ತು ಕಳುಹಿಸುವವರು ಮುಂದಿನ ಕಳುಹಿಸುವಿಕೆಯನ್ನು ನಿರ್ಬಂಧಿಸುತ್ತಾರೆ. ಚಾನೆಲ್ಗಳ ನಡುವೆ ಯಾವುದೇ ಸಾಮಾನ್ಯ ಸಂದೇಶ ಬಫರ್ ಹಂಚಿಕೆಯಾಗಿಲ್ಲ ಎಂಬುದನ್ನು ಗಮನಿಸಿ. ಹೆಚ್ಚುತ್ತಿರುವ ಸಂಕೀರ್ಣತೆ, ಒಂದು ಚಾನೆಲ್ ಅನ್ನು ಏಕಮುಖವಾಗಿ ಮತ್ತು ಬಿಂದುವಿನಿಂದ ಬಿಂದುವಿಗೆ ಬಳಸುವುದಕ್ಕೆ ಹೋಲಿಸಿದರೆ, ಅನೇಕ ಸ್ವೀಕರಿಸುವವರು ಅಥವಾ ಬಹು ಕಳುಹಿಸುವವರ ನಡುವೆ ಚಾನೆಲ್ಗಳನ್ನು ಹಂಚಿಕೊಳ್ಳಲು ಮತ್ತು ಸ್ವತಂತ್ರ ಡೇಟಾ-ಸ್ಟ್ರೀಮ್ಗಳನ್ನು ಒಂದೇ ಹಂಚಿಕೆಯ ಚಾನೆಲ್ನಲ್ಲಿ ವಿಲೀನಗೊಳಿಸಲು ಸಾಧ್ಯವಿದೆ. ಇದರಿಂದ ಎರಡು ದಿಕ್ಕುಗಳ ಸಂವಹನಕ್ಕೂ ಒಂದೇ ಮಾರ್ಗವನ್ನು ಬಳಸಬಹುದಾಗಿದೆ. ನಿಯಂತ್ರಣ ಹರಿವಿನ ರಚನೆಗಳು ಪ್ರೋಮೆಲಾದಲ್ಲಿ ಮೂರು ನಿಯಂತ್ರಣ ಹರಿವಿನ ರಚನೆಗಳಿವೆ. ಅವುಗಳೆಂದರೆ ಕೇಸ್ ಆಯ್ಕೆ, ಪುನರಾವರ್ತನೆ ಮತ್ತು ಬೇಷರತ್ತಾದ ಜಿಗಿತ. ಕೇಸ್ ಆಯ್ಕೆಯು ಅತ್ಯಂತ ಸರಳವಾದ ರಚನೆಯೆಂದರೆ ಆಯ್ಕೆ ರಚನೆಯಾಗಿದೆ. ಉದಾಹರಣೆಗೆ, a ಮತ್ತು b ಎಂಬ ಎರಡು ಅಸ್ಥಿರಗಳ ಸಾಪೇಕ್ಷ ಮೌಲ್ಯಗಳನ್ನು ಬಳಸಿಕೊಂಡು, ಒಬ್ಬರು ಹೀಗೆ ಬರೆಯಬಹುದುಃ: (a! = b)-> ಆಯ್ಕೆ1:: (a = = b)-> ಆಯ್ಕೆ2 ಫೈ ಆಯ್ಕೆಯ ರಚನೆಯು ಎರಡು ಕಾರ್ಯಗತಗೊಳಿಸುವ ಅನುಕ್ರಮಗಳನ್ನು ಹೊಂದಿರುತ್ತದೆ, ಪ್ರತಿಯೊಂದಕ್ಕೂ ಮೊದಲು ಡಬಲ್ ಕೊಲಾನ್ ಇರುತ್ತದೆ. ಪಟ್ಟಿಯಿಂದ ಒಂದು ಅನುಕ್ರಮವನ್ನು ಕಾರ್ಯಗತಗೊಳಿಸಲಾಗುತ್ತದೆ. ಅದರ ಮೊದಲ ಹೇಳಿಕೆಯನ್ನು ಕಾರ್ಯಗತಗೊಳಿಸಬಹುದಾದರೆ ಮಾತ್ರ ಅನುಕ್ರಮವನ್ನು ಆಯ್ಕೆ ಮಾಡಬಹುದು. ನಿಯಂತ್ರಣ ಅನುಕ್ರಮದ ಮೊದಲ ಹೇಳಿಕೆಯನ್ನು ಕಾವಲುಗಾರ ಎಂದು ಕರೆಯಲಾಗುತ್ತದೆ. ಮೇಲಿನ ಉದಾಹರಣೆಯಲ್ಲಿ, ಕಾವಲುಗಾರರು ಪರಸ್ಪರ ಪ್ರತ್ಯೇಕವಾಗಿರುತ್ತಾರೆ, ಆದರೆ ಅವರು ಇರಬೇಕಾಗಿಲ್ಲ. ಒಂದಕ್ಕಿಂತ ಹೆಚ್ಚು ಗಾರ್ಡ್ಗಳನ್ನು ಕಾರ್ಯಗತಗೊಳಿಸಬಹುದಾದರೆ, ಅನುಗುಣವಾದ ಅನುಕ್ರಮಗಳಲ್ಲಿ ಒಂದನ್ನು ನಿರ್ಣಾಯಕವಲ್ಲದ ರೀತಿಯಲ್ಲಿ ಆಯ್ಕೆ ಮಾಡಲಾಗುತ್ತದೆ. ಎಲ್ಲಾ ಕಾವಲುಗಾರರನ್ನು ಕಾರ್ಯಗತಗೊಳಿಸಲಾಗದಿದ್ದರೆ, ಅವರಲ್ಲಿ ಒಬ್ಬರನ್ನು ಆಯ್ಕೆ ಮಾಡುವವರೆಗೆ ಪ್ರಕ್ರಿಯೆಯು ನಿರ್ಬಂಧಿಸುತ್ತದೆ. (ಇದಕ್ಕೆ ವಿರುದ್ಧವಾಗಿ, ಆಕಾಮ್ ಪ್ರೋಗ್ರಾಮಿಂಗ್ ಭಾಷೆಯು ನಿಲ್ಲುತ್ತದೆ ಅಥವಾ ಯಾವುದೇ ಕಾರ್ಯಗತಗೊಳಿಸಬಹುದಾದ ಗಾರ್ಡ್ಗಳಿಲ್ಲದೆ ಮುಂದುವರಿಯಲು ಸಾಧ್ಯವಾಗುವುದಿಲ್ಲ.) ವೇಳೆಃ: (A = = ನಿಜ)-> ಆಯ್ಕೆ1;:: (B = = ನಿಜ)-> ಆಯ್ಕೆ2;/* A = = ನಿಜ */:: ಇಲ್ಲದಿದ್ದರೆ-> ಫಾಲ್ ಥ್ರೂ _ ಆಯ್ಕೆ; fi ಆಗಿದ್ದರೆ ಸಹ ಇಲ್ಲಿಗೆ ಬರಬಹುದು. "ಸಾಂಪ್ರದಾಯಿಕ" ಪ್ರೋಗ್ರಾಮಿಂಗ್ ನಲ್ಲಿ, ಒಂದು ಇಫ್-ಇಫ್-ಎಲ್ಸ್ ರಚನೆಯನ್ನು ಅನುಕ್ರಮವಾಗಿ ಅರ್ಥಮಾಡಿಕೊಳ್ಳಬಹುದು. ಇಲ್ಲಿ, ಇಫ್-ಡಬಲ್ ಕೊಲೊನ್-ಡಬಲ್ ಕೊಲೊನ್ ಅನ್ನು "ಯಾವುದಾದರೂ ಸಿದ್ಧವಾಗಿದೆ" ಎಂದು ಅರ್ಥೈಸಿಕೊಳ್ಳಬೇಕು ಮತ್ತು ಯಾವುದೂ ಸಿದ್ಧವಾಗಿಲ್ಲದಿದ್ದರೆ, ನಂತರವೇ ಉಳಿದವುಗಳನ್ನು ತೆಗೆದುಕೊಳ್ಳಲಾಗುತ್ತದೆ. ವೇಳೆಃ: ಮೌಲ್ಯ = 3;:: ಮೌಲ್ಯ = 4; ಫೈ ಮೇಲಿನ ಉದಾಹರಣೆಯಲ್ಲಿ, ಮೌಲ್ಯವನ್ನು ನಿರ್ಣಾಯಕವಾಗಿ 3 ಅಥವಾ 4 ಮೌಲ್ಯವನ್ನು ನೀಡಲಾಗುವುದಿಲ್ಲ. ಕಾವಲುಗಾರರಾಗಿ ಬಳಸಬಹುದಾದ ಎರಡು ಹುಸಿ ಹೇಳಿಕೆಗಳಿವೆಃ ಟೈಮ್ಔಟ್ ಹೇಳಿಕೆ ಮತ್ತು ಎಲ್ಸ್ ಹೇಳಿಕೆ. ಟೈಮ್ಔಟ್ ಹೇಳಿಕೆಯು ವಿಶೇಷ ಸ್ಥಿತಿಯನ್ನು ರೂಪಿಸುತ್ತದೆ, ಅದು ಎಂದಿಗೂ ನಿಜವಾಗದ ಸ್ಥಿತಿಯ ಕಾಯುವಿಕೆಯನ್ನು ಸ್ಥಗಿತಗೊಳಿಸಲು ಪ್ರಕ್ರಿಯೆಯನ್ನು ಅನುಮತಿಸುತ್ತದೆ. ಬೇರೆ ಹೇಳಿಕೆಯನ್ನು ಆಯ್ಕೆ ಅಥವಾ ಪುನರಾವರ್ತನೆ ಹೇಳಿಕೆಯಲ್ಲಿ ಕೊನೆಯ ಆಯ್ಕೆಯ ಅನುಕ್ರಮದ ಆರಂಭಿಕ ಹೇಳಿಕೆಯಾಗಿ ಬಳಸಬಹುದು. ಒಂದೇ ಆಯ್ಕೆಯಲ್ಲಿರುವ ಎಲ್ಲಾ ಇತರ ಆಯ್ಕೆಗಳು ಕಾರ್ಯಗತಗೊಳ್ಳದಿದ್ದರೆ ಮಾತ್ರ ಎಲ್ಸ್ ಅನ್ನು ಕಾರ್ಯಗತಗೊಳಿಸಬಹುದು. ಅಲ್ಲದೆ, ಎಲ್ಸ್ ಅನ್ನು ಚಾನೆಲ್ಗಳೊಂದಿಗೆ ಒಟ್ಟಾಗಿ ಬಳಸಲಾಗುವುದಿಲ್ಲ. ಪುನರಾವರ್ತನೆ (ಲೂಪ್) ಆಯ್ಕೆ ರಚನೆಯ ತಾರ್ಕಿಕ ವಿಸ್ತರಣೆಯು ಪುನರಾವರ್ತನೆಯ ರಚನೆಯಾಗಿದೆ. ಉದಾಹರಣೆಗೆಃ ಡುಃಃ ಕೌಂಟ್ = ಕೌಂಟ್ + 1:: a = b + 2:: (ಕೌಂಟ್ = = 0)-> ಬ್ರೇಕ್ od ಎಂಬುದು ಪ್ರೋಮೆಲಾದಲ್ಲಿ ಪುನರಾವರ್ತನೆಯ ರಚನೆಯನ್ನು ವಿವರಿಸುತ್ತದೆ. ಒಂದು ಸಮಯದಲ್ಲಿ ಒಂದು ಆಯ್ಕೆಯನ್ನು ಮಾತ್ರ ಆಯ್ಕೆ ಮಾಡಬಹುದು. ಆಯ್ಕೆಯು ಪೂರ್ಣಗೊಂಡ ನಂತರ, ರಚನೆಯ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯನ್ನು ಪುನರಾವರ್ತಿಸಲಾಗುತ್ತದೆ. ಪುನರಾವರ್ತನೆಯ ರಚನೆಯನ್ನು ಕೊನೆಗೊಳಿಸುವ ಸಾಮಾನ್ಯ ಮಾರ್ಗವೆಂದರೆ ವಿರಾಮ ಹೇಳಿಕೆಯಾಗಿದೆ. ಇದು ನಿಯಂತ್ರಣವನ್ನು ಪುನರಾವರ್ತನೆಯ ರಚನೆಯನ್ನು ತಕ್ಷಣವೇ ಅನುಸರಿಸುವ ಸೂಚನೆಗೆ ವರ್ಗಾಯಿಸುತ್ತದೆ. ಷರತ್ತು ರಹಿತ ಜಿಗಿತಗಳು ಲೂಪ್ ಅನ್ನು ಮುರಿಯಲು ಮತ್ತೊಂದು ಮಾರ್ಗವೆಂದರೆ ಗೋಟೋ ಹೇಳಿಕೆ. ಉದಾಹರಣೆಗೆ, ಮೇಲಿನ ಉದಾಹರಣೆಯನ್ನು ಈ ಕೆಳಗಿನಂತೆ ಮಾರ್ಪಡಿಸಬಹುದುಃ ಹೀಗೆ ಮಾಡಿಃಃ ಎಣಿಕೆ = ಎಣಿಕೆ + 1:: a = b + 2:: (ಎಣಿಕೆ = = 0)-> ಪೂರ್ಣಗೊಂಡಿದೆ. ಒಂದು ಹೇಳಿಕೆಯ ಮೊದಲು ಮಾತ್ರ ಲೇಬಲ್ ಕಾಣಿಸಿಕೊಳ್ಳಬಹುದು. ಕಾರ್ಯಕ್ರಮದ ಕೊನೆಯಲ್ಲಿ ಜಿಗಿಯಲು, ಉದಾಹರಣೆಗೆ, ಡಮ್ಮಿ ಸ್ಟೇಟ್ಮೆಂಟ್ ಸ್ಕಿಪ್ ಉಪಯುಕ್ತವಾಗಿದೆಃ ಇದು ಯಾವಾಗಲೂ ಕಾರ್ಯಗತಗೊಳಿಸಬಹುದಾದ ಮತ್ತು ಯಾವುದೇ ಪರಿಣಾಮವನ್ನು ಹೊಂದಿರದ ಪ್ಲೇಸ್-ಹೋಲ್ಡರ್ ಆಗಿದೆ. ಸಮರ್ಥನೆಗಳು ಸ್ವಲ್ಪ ವಿವರಣೆಯ ಅಗತ್ಯವಿರುವ ಪ್ರೊಮೆಲಾದಲ್ಲಿನ ಒಂದು ಪ್ರಮುಖ ಭಾಷಾ ರಚನೆಯೆಂದರೆ ದೃಢವಾದ ಹೇಳಿಕೆ. ಫಾರ್ಮ್ನ ಹೇಳಿಕೆಗಳುಃ ಅಸ್ಸೇರ್ಟ್ (ಯಾವುದೇ _ ಬೂಲಿಯನ್ _ ಷರತ್ತು) ಯಾವಾಗಲೂ ಕಾರ್ಯಗತಗೊಳ್ಳಬಲ್ಲವು. ನಿರ್ದಿಷ್ಟಪಡಿಸಿದ ಬೂಲಿಯನ್ ಸ್ಥಿತಿಯು ಇದ್ದರೆ, ಹೇಳಿಕೆಯು ಯಾವುದೇ ಪರಿಣಾಮವನ್ನು ಬೀರುವುದಿಲ್ಲ. ಆದಾಗ್ಯೂ, ಷರತ್ತು ಅಗತ್ಯವಾಗಿ ಇಲ್ಲದಿದ್ದರೆ, ಹೇಳಿಕೆಯು ಸ್ಪಿನ್ ನೊಂದಿಗೆ ಪರಿಶೀಲನೆಯ ಸಮಯದಲ್ಲಿ ದೋಷವನ್ನು ಉಂಟುಮಾಡುತ್ತದೆ. ಸಂಕೀರ್ಣ ದತ್ತಾಂಶ ರಚನೆಗಳು ಪೂರ್ವನಿರ್ಧರಿತ ಅಥವಾ ಹಿಂದಿನ ವ್ಯಾಖ್ಯಾನಿತ ಪ್ರಕಾರಗಳ ದತ್ತಾಂಶ ವಸ್ತುಗಳ ಪಟ್ಟಿಗೆ ಹೊಸ ಹೆಸರನ್ನು ಪರಿಚಯಿಸಲು ಪ್ರೋಮೆಲಾ ವ್ಯಾಖ್ಯಾನವನ್ನು ಬಳಸಬಹುದು. ಹೊಸ ರೀತಿಯ ಹೆಸರನ್ನು ಹೊಸ ಡೇಟಾ ಆಬ್ಜೆಕ್ಟ್ಗಳನ್ನು ಘೋಷಿಸಲು ಮತ್ತು ತ್ವರಿತಗೊಳಿಸಲು ಬಳಸಬಹುದು, ಇದನ್ನು ಯಾವುದೇ ಸಂದರ್ಭದಲ್ಲಿ ಸ್ಪಷ್ಟ ರೀತಿಯಲ್ಲಿ ಬಳಸಬಹುದುಃ ಟೈಪೆಡೆಫ್ ನಿರ್ಮಾಣದಲ್ಲಿ ಘೋಷಿಸಲಾದ ಕ್ಷೇತ್ರಗಳಿಗೆ ಪ್ರವೇಶವನ್ನು ಸಿ ಪ್ರೋಗ್ರಾಮಿಂಗ್ ಭಾಷೆಯಂತೆಯೇ ಮಾಡಲಾಗುತ್ತದೆ. ಉದಾಹರಣೆಗೆಃ MyStruct x; x.Field1 = 1; ಇದು ಮಾನ್ಯವಾದ PROMELA ಅನುಕ್ರಮವಾಗಿದ್ದು, ಇದು x ವೇರಿಯೇಬಲ್ನ ಫೀಲ್ಡ್ 1 ಗೆ 1 ಮೌಲ್ಯವನ್ನು ನಿಯೋಜಿಸುತ್ತದೆ. ಸಕ್ರಿಯ ಪ್ರಾಕ್ಟೈಪ್ಗಳು ಸಕ್ರಿಯ ಕೀವರ್ಡ್ ಅನ್ನು ಯಾವುದೇ ಪ್ರಾಕ್ಟೈಪ್ ವ್ಯಾಖ್ಯಾನಕ್ಕೆ ಪೂರ್ವಪ್ರತ್ಯಯ ಮಾಡಬಹುದು. ಕೀವರ್ಡ್ ಇದ್ದರೆ, ಆ ಪ್ರಾಕ್ಟೈಪ್ನ ಒಂದು ಉದಾಹರಣೆಯು ಆರಂಭಿಕ ಸಿಸ್ಟಮ್ ಸ್ಥಿತಿಯಲ್ಲಿ ಸಕ್ರಿಯವಾಗಿರುತ್ತದೆ. ಆ ಪ್ರಾಕ್ಟೈಪ್ನ ಬಹು ಕ್ಷಣಗಳನ್ನು ಕೀವರ್ಡ್ನ ಐಚ್ಛಿಕ ಶ್ರೇಣಿಯ ಪ್ರತ್ಯಯದೊಂದಿಗೆ ನಿರ್ದಿಷ್ಟಪಡಿಸಬಹುದು. ಉದಾಹರಣೆಃ ಸಕ್ರಿಯ ಪ್ರಾಕ್ಟೈಪ್ ಎ () {.} ಸಕ್ರಿಯ [4] ಪ್ರಾಕ್ಟೈಪ್ ಬಿ () {.} ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯ ಶಬ್ದಾರ್ಥವು ಪ್ರೊಮೆಲಾದಲ್ಲಿ ಮಾಡೆಲಿಂಗ್ ಪ್ರಕ್ರಿಯೆಯ ಸಿಂಕ್ರೊನೈಸೇಶನ್ಗಳಿಗೆ ಮೂಲ ವಿಧಾನವನ್ನು ಒದಗಿಸುತ್ತದೆ. mtype = {M _ UP, M _ DW}; chan Chan _ ಡೇಟಾ _ ಡೌನ್ = [0] ಆಫ್ {mtype}; chan Chan _ ಡೇಟಾ _ ಅಪ್ = [0] ಆಫ್ {mtype}; ಪ್ರಾಕ್ಟೈಪ್ P1 (chan Chan _ ಡೇಟಾ _ ಇನ್, Chan _ ಡೇಟಾ _ ಔಟ್) {ಡುಃ: Chan _ ಡೇಟಾ _ ಇನ್? M _ UP-> ಬಿಟ್ಟುಬಿಡಿ;:: Chan _ Data _ out! M _ DW-> ಸ್ಕಿಪ್; od;}; ಪ್ರಾಕ್ಟೈಪ್ P2 (ಚಾನ್ಚಾನ್ _ ಡೇಟಾ _ ಇನ್, ಚಾನ್ಚಾನ್ _ ಡೇಟಾ _ ಔಟ್) {ಡುಃ: ಚಾನ್ಚಾನ್ _ ಡೇಟಾ _ ಇನ್? M _ DW-> ಬಿಟ್ಟುಬಿಡಿ;:: Chan _ Data _ out! M _ UP-> ಸ್ಕಿಪ್; od;}; init {atomic {ರನ್ P1 (ಚಾನ _ ಡೇಟಾ _ ಅಪ್, ಚಾನ _ ಡೇಟಾ _ ಡೌನ್); ರನ್ P2 (ಚಾನ _ ಡೇಟಾ _ ಡೌನ್, ಚಾನ _ ಡೇಟಾ _ ಅಪ್);}} ಉದಾಹರಣೆಯಲ್ಲಿ, P1 ಮತ್ತು P2 ಎಂಬ ಎರಡು ಪ್ರಕ್ರಿಯೆಗಳು (1) ಇನ್ನೊಂದರಿಂದ ಇನ್ಪುಟ್ ಅಥವಾ (2) ಇನ್ನೊಂದಕ್ಕೆ ಔಟ್ಪುಟ್ನ ನಿರ್ಣಾಯಕವಲ್ಲದ ಆಯ್ಕೆಗಳನ್ನು ಹೊಂದಿವೆ. ಎರಡು ಸಂಧಿಸುವ ಹಸ್ತಲಾಘವಗಳು ಸಾಧ್ಯ, ಅಥವಾ ಕಾರ್ಯಗತಗೊಳಿಸಬಹುದಾದವು, ಮತ್ತು ಅವುಗಳಲ್ಲಿ ಒಂದನ್ನು ಆಯ್ಕೆ ಮಾಡಲಾಗುತ್ತದೆ. ಇದು ಶಾಶ್ವತವಾಗಿ ಪುನರಾವರ್ತನೆಯಾಗುತ್ತದೆ. ಆದ್ದರಿಂದ, ಈ ಮಾದರಿಯು ಸ್ಥಗಿತಗೊಳ್ಳುವುದಿಲ್ಲ. ಮೇಲಿನ ಮಾದರಿಯನ್ನು ಸ್ಪಿನ್ ವಿಶ್ಲೇಷಿಸಿದಾಗ, ಅದು ನಿರ್ಧಾರಕವಲ್ಲದ ಅಲ್ಗಾರಿದಮ್ನೊಂದಿಗೆ ಆಯ್ಕೆಗಳನ್ನು ಪರಿಶೀಲಿಸುತ್ತದೆ, ಅಲ್ಲಿ ಎಲ್ಲಾ ಕಾರ್ಯಗತಗೊಳಿಸಬಹುದಾದ ಆಯ್ಕೆಗಳನ್ನು ಅನ್ವೇಷಿಸಲಾಗುತ್ತದೆ. ಆದಾಗ್ಯೂ, ಸ್ಪಿನ್ ಸಿಮ್ಯುಲೇಟರ್ ಸಂಭವನೀಯ ಪರಿಶೀಲಿಸದ ಸಂವಹನ ಮಾದರಿಗಳನ್ನು ದೃಶ್ಯೀಕರಿಸಿದಾಗ, ಅದು "ನಿರ್ಣಾಯಕವಲ್ಲದ" ಆಯ್ಕೆಯನ್ನು ಪರಿಹರಿಸಲು ಯಾದೃಚ್ಛಿಕ ಜನರೇಟರ್ ಅನ್ನು ಬಳಸಬಹುದು. ಆದ್ದರಿಂದ, ಸಿಮ್ಯುಲೇಟರ್ ಕೆಟ್ಟ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯನ್ನು ತೋರಿಸಲು ವಿಫಲವಾಗಬಹುದು (ಉದಾಹರಣೆಗೆ, ಯಾವುದೇ ಕೆಟ್ಟ ಜಾಡು ಇಲ್ಲ). ಇದು ಪರಿಶೀಲನೆ ಮತ್ತು ಅನುಕರಣೆಯ ನಡುವಿನ ವ್ಯತ್ಯಾಸವನ್ನು ವಿವರಿಸುತ್ತದೆ. ಇದಲ್ಲದೆ, ಪರಿಷ್ಕರಣೆಯನ್ನು ಬಳಸಿಕೊಂಡು ಪ್ರೋಮೆಲಾ ಮಾದರಿಗಳಿಂದ ಕಾರ್ಯಗತಗೊಳಿಸಬಹುದಾದ ಕೋಡ್ ಅನ್ನು ರಚಿಸಲು ಸಹ ಸಾಧ್ಯವಿದೆ. ಕೀವರ್ಡ್ಗಳು ಈ ಕೆಳಗಿನ ಗುರುತಿಸುವಿಕೆಗಳನ್ನು ಕೀವರ್ಡ್ಗಳಾಗಿ ಬಳಸಲು ಕಾಯ್ದಿರಿಸಲಾಗಿದೆ. ಉಲ್ಲೇಖಗಳು ಬಾಹ್ಯ ಕೊಂಡಿಗಳು ಸ್ಪಿನ್ ಮುಖಪುಟ ಸ್ಪಿನ್ ಟ್ಯುಟೋರಿಯಲ್ಗಳು ಮತ್ತು ಆನ್ಲೈನ್ ಉಲ್ಲೇಖಗಳು ಸಂಕ್ಷಿಪ್ತ ಪ್ರೋಮೆಲಾ ರೆಫರೆನ್ಸ್ ಕಂಪ್ಯೂಟರ್ ನೆರವಿನ ಸ್ವಯಂಚಾಲಿತ ಪರಿಶೀಲನೆಃ "ದಿ ಸಿಎವಿಎ ಪ್ರಾಜೆಕ್ಟ್" (2010-2019) ಮತ್ತು "ವೆರಿಫೈಡ್ ಮಾಡೆಲ್ ಚೆಕರ್ಸ್" (2016-ಕ್ಯೂಆರ್ಆರ್) ಜಾಲತಾಣ ಸ್ಪೆಸಿಫಿಕೇಷನ್ ಲಾಂಗ್ವೇಜಸ್ ಮಾಡೆಲ್ ಚೆಕರ್ಸ್