acc concurrency

• Interleaving: processors running in 'parallel' by being divided up and scheduled
• || is used to represent concurrent execution (P || Q)

  
• Concurrent compositions are created by: kind of creating a powerset of all possible options and states

  
• || is commutative (reverse has the same result )and associative (any order of stacking has the same result)

  
• || NAME = (a:NAME || b:NAME) mashes 2 NAME together concurrently in a cartesian way (just a powerset)
• a:NAME = creating an naming one instance of a process
• a:NAME = creating an naming one instance of a process

  
• Can combine ranges and labelling to generate many labelled states (s[i:0..4]:NAME) or use a forall (forall[i:0..4] s[i]:NAME)

  
• Concurrency happens through actions completed together or resource sharing

  
• For common/shared action, all prerequisite actions on both sides must be completed for it to continue. There are still states and actions for every possible order of the actions being carried out

  
• Sometimes, concurrent composition LTSA can also be described using simply guards
• ::NAME is used to denote a process that is a shared resource, {a,b} is a label showing that it could be either a or b doing ti

  
• Shared resources also enforce combining common actions, but make sure these make sense and arent just all cartesian product

  
• {a,b} labels allow the combination that allows it to be correctly drawn

  
• actions are relabelled to match across being called different things in different models using /{name1/name2,...,} (where name2 gets dropped)

  
• every labelled instance's actions must be renamed individually

  
• safety is actually: A safety property P defines a deterministic process that asserts that any trace including actions in the alphabet of P, is accepted by P
• \ - hide an action that the user does not need to see, eg instead of combining use with print just hide print

  
• tau = not relevant in the current model context
• @ - inference (fully removes an action from the alphabet)
• Yield() - Thread relinquishes control so someone else can go instead
• Counters etc. can be modelled as simple read/write memory states

  
• can have independently looping loops

  
• process

  
• iurhiure